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 KE

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