Provador de teoremas
De Wiki DAINF
(Diferença entre revisões)
(→Alguns links sobre provadores de teoremas) |
(→Páginas de Provadores de Teoremas) |
||
Linha 16: | Linha 16: | ||
* [http://www.cs.unm.edu/~mccune/eqp/ EQP - Equational Prover] | * [http://www.cs.unm.edu/~mccune/eqp/ EQP - Equational Prover] | ||
+ | ** "EQP is an automated theorem proving program for first-order equational logic." | ||
* [http://www.cs.unm.edu/~mccune/otter/ Otter e Mace2] | * [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." | ** "Otter is an automated theorem prover for first-order and equational logic, and Mace2 searches for finite models and counterexamples." |
Edição de 14h24min de 22 de abril de 2009
Alguns links sobre provadores de teoremas
Páginas de Provadores de Teoremas
- 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."