Isabelle

http://pt.dbpedia.org/resource/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.
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. 
xsd:nonNegativeInteger 24 
xsd:integer 1151724 
xsd:nonNegativeInteger 2183 
xsd:integer 36024141 

data from the linked data cloud