Provador de teoremas
De Wiki DAINF
(Diferença entre revisões)
(→Páginas de Provadores de Teoremas) |
(→Páginas de Provadores de Teoremas) |
||
| Linha 14: | Linha 14: | ||
=== Páginas de Provadores de Teoremas === | === Páginas de Provadores de Teoremas === | ||
| + | |||
| + | |||
| + | ==== Baseados no Método da Resolução ==== | ||
* [http://www.cs.unm.edu/~mccune/eqp/ EQP - Equational Prover] | * [http://www.cs.unm.edu/~mccune/eqp/ EQP - Equational Prover] | ||
| Linha 22: | Linha 25: | ||
* [http://www.cs.unm.edu/~mccune/prover9/ Prover8 e Mace4] | * [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." | ** "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 ===== | ||
| + | |||
| + | * [http://www.dainf.ct.utfpr.edu.br/~adolfo/KEMS/ KEMS is a KE-based Multi-Strategy theorem prover.] | ||
Edição de 13h26min de 22 de abril de 2009
Tabela de conteúdo |
Alguns links sobre provadores de teoremas
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."
