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.^[2][3]

Isabelle
Autor	Lawrence Paulson
Desenvolvedores	Universidade de Cambridge e Universidade Técnica de Munique et al.
Lançamento inicial	1986[1]
Escrito em	Standard ML e Scala
Sistema operacional	Linux, Windows, macOS
Tipo	Matemática
Licença	Licença BSD
Website	isabelle.in.tum.de

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.^[3][4][5]

Referências

1. Paulson, L. C. (1986). «Natural deduction as higher-order resolution». The Journal of Logic Programming. 3 (3): 237–258. arXiv:cs/9301104. doi:10.1016/0743-1066(86)90015-4
2. Eberl, Manuel; Klein, Gerwin; Nipkow, Tobias; Paulson, Larry; Thiemann, René. «Archive of Formal Proofs». Consultado em 1 de maio de 2021
3. Gordon, Mike (16 de novembro de 1994). «1.2 History». Isabelle and HOL. Cambridge AR Research (The Automated Reasoning Group). Consultado em 28 de abril de 2016
4. Jasmin Christian Blanchette, Lukas Bulwahn, Tobias Nipkow, "Automatic Proof and Disproof in Isabelle/HOL", in: Cesare Tinelli, Viorica Sofronie-Stokkermans (eds.), International Symposium on Frontiers of Combining Systems – FroCoS 2011, Springer, 2011.
5. Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli, "Model Finding for Recursive Functions in SMT", in: Nicola Olivetti, Ashish Tiwari (eds.), 8th International Joint Conference on Automated Reasoning, Springer, 2016.