Isabelle

Isabelle é um programa de computador utilizado para processar fórmulas matemáticas. Foi desenvolvido por um Lawrence C. Paulson (Univ. of Cambridge, UK) e Tobias Nipkow (Technical Univ. of Munich, DE). Trata-se de um ambiente de demostrações que permite a representação e o uso de diversos sistemas de como Pure, ZF, FOL, estruturado por uma meta-ló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ígüos; 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.

Ligações externas

• «Site oficial da ferramenta» (em English) 
• «Site da camada Isar (interface)» (em Deutsch) 
• «Ambiente itegrante do Isabelle/Isar (utiliza o ambiente X emacs)» (em English)