Isabelle
Origem: Wikipédia, a enciclopédia livre.
| Este artigo ou seção precisa ser wikificado. Por favor ajude a formatar este artigo de acordo com as diretrizes estabelecidas no livro de estilo. (Fevereiro de 2008) |
[editar] Origem
Isabelle 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.
[editar] Ligações Externas
- Isabelle Site oficial da ferramenta
- Isar Site da camada Isar (interface)
- ProofGeneral Ambiente itegrante do Isabelle/Isar (utiliza o ambiente [X]emacs)
