Isabelle
# Isabelle

Isabelle é um programa de computador utilizado para processar fórmulas matemáticas. Foi desenvolvido por um Lawrence C. Paulson (da Universidade de Cambridge, no Reino Unido) e Tobias Nipkow (da Universidade Técnica de Munique, na Alemanha). Trata-se de um ambiente de demonstrações que permite a representação e o uso de diversos sistemas como Pure, ZF, FOL, estruturado por uma metalógica intuicionista de ordem superior.
As regras de derivação podem ser especificadas em diferentes formatos, como por exemplo, dedução natural, axiomática hilbertiana, sistema de seqüentes, tablôs, dentre outras, e possui três componentes principais: uma meta-implicação que possibilita o uso de regras da lógica-objeto específica e que é responsável pela aplicação dessas regras e no resultado das suposições; uma meta-quantificação universal sobre inúmeros quantificadores da linguagem-objeto; uma meta-igualdade que torna uma abreviação apenas uma maneira de reescrever regras. Pode ser visto como um provador de teoremas automatizável onde: lógica-objetos são λ-termos cuja gramática de prioridades os torna não ambíguos; regras da linguagem-objeto não são representadas como funções, mas como fórmulas da lógica de ordem superior; a combinação e aplicação dessas regras são executadas por um método uniforme de inferência, a resolução de ordem superior; táticas são implementadas independentemente da lógica-objeto representada.