Isabelle
| Isabelle | |
|---|---|
 | |
| Autor | Lawrence Paulson |
| Desenvolvedor | Universidade de Cambridge e Universidade Técnica de Munique et al. |
| Lançamento | 1986[1] |
| Escrito em | Standard ML e Scala |
| Sistema operacional | Linux, Windows, macOS |
| Gênero(s) | Matemática |
| Licença | Licença BSD |
| Página oficial | 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]
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
- ↑ 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
- ↑ Eberl, Manuel; Klein, Gerwin; Nipkow, Tobias; Paulson, Larry; Thiemann, René. «Archive of Formal Proofs». Consultado em 1 de maio de 2021
- ↑ a b 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
- ↑ 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.
- ↑ 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.
Ligações externas[editar | editar código-fonte]
- «Site oficial da ferramenta» (em inglês)
- «Site da camada Isar (interface)» (em alemão)
- «Ambiente itegrante do Isabelle/Isar (utiliza o ambiente X emacs)» (em inglês)
