Provador de teoremas

De Wiki DAINF

(Diferença entre revisões)

Edição de 14h24min de 22 de abril de 2009

EQP - Equational Prover
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."

@@ Linha 4: / Linha 4: @@
 ** [http://www.cs.unm.edu/~mccune/papers/robbins/nyt-corrections.html Correções técnicas à notícia acima]
 ** [http://www.cs.unm.edu/~mccune/papers/robbins/ "Robbins Algebras Are Boolean", página de William McCune sobre o resultado acima]
+** [http://mathworld.wolfram.com/RobbinsConjecture.html Descrição da Conjetura de Robbins]
+** [http://en.wikipedia.org/wiki/Robbins_algebra Robbins Algebra na Wikipedia]
+* [http://cnx.org/content/m12074/latest/ Limitações das tabelas-verdade]
+* [http://www.geocities.com/logicfuzby/index.htm Lógicas não-clássicas (trabalho de estudantes da PUC-PR)]
 === Páginas de Provadores de Teoremas ===
 * [http://www.cs.unm.edu/~mccune/eqp/ EQP - Equational Prover]
-* [
+* [http://www.cs.unm.edu/~mccune/otter/ Otter e Mace2]
+** "Otter is an automated theorem prover for first-order and equational logic, and Mace2 searches for finite models and counterexamples."
+** [http://en.wikipedia.org/wiki/Otter_theorem_prover Artigo sobre o Otter na Wikipedia]
+* [http://www.cs.unm.edu/~mccune/prover9/ 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."