Provador de teoremas

Alguns links sobre provadores de teoremas

• "Computer Math Proof Shows Reasoning Power", notícia do New York Times de 10/12/1996 comentando um importante resultado matemático obtido por um provador de teoremas
  • Correções técnicas à notícia acima
  • "Robbins Algebras Are Boolean", página de William McCune sobre o resultado acima
  • Descrição da Conjetura de Robbins
  • Robbins Algebra na Wikipedia

• Limitações das tabelas-verdade

• Lógicas não-clássicas (trabalho de estudantes da PUC-PR)

Páginas de Provadores de Teoremas

Baseados no Método da Resolução

• EQP - Equational Prover
  • "EQP is an automated theorem proving program for first-order equational logic."
• Otter e Mace2
  • "Otter is an automated theorem prover for first-order and equational logic, and Mace2 searches for finite models and counterexamples."
  • Artigo sobre o Otter na Wikipedia
• Prover8 e Mace4
  • "Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples. Prover9 is the successor of the Otter prover."

Baseados em Tablôs

Baseados em Tablôs Analíticos

• jTAP - A Tableau Prover in Java
  • "jTAP is a propositional tableau prover. It is implemented in Java and supports in its current version classical propositional logic, but it is easily extendable. The prover is described in the Unified Modeling Language (UML), an object-oriented modeling language. You can find some UML diagrams in the appendix of the jTAP documentation, which may help to understand the architecture of the prover and how it works."

• WDTP - Wagner Dias Tableau Prover

Baseados em Tablôs KE

• KEMS is a KE-based Multi-Strategy theorem prover.