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 14h26min 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."

Baseados em Tablôs

Baseados em Tablôs KE
Ferramentas pessoais