Provador de teoremas
De Wiki DAINF
(Diferença entre revisões)
(→Alguns links sobre provadores de teoremas) |
(→Baseados em Tablôs KE) |
||
(10 edições intermediárias de um usuário não apresentadas) | |||
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/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://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 === | === 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] | ||
− | * [ | + | ** "EQP is an automated theorem proving program for first-order equational logic." |
+ | * [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." | ||
+ | |||
+ | ==== Baseados em Tablôs ==== | ||
+ | |||
+ | ===== Baseados em Tablôs Analíticos ===== | ||
+ | |||
+ | * [http://i12www.ira.uka.de/~aroth/jTAP/ jTAP - A Tableau Prover in Java] | ||
+ | ** "jTAP is a propositional tableau prover. It is implemented in Java and supports in its current version classical propositional logic, but it is easily extendable. The prover is described in the Unified Modeling Language (UML), an object-oriented modeling language. You can find some UML diagrams in the appendix of the jTAP documentation, which may help to understand the architecture of the prover and how it works." | ||
+ | |||
+ | * [[WDTP - Wagner Dias Tableau Prover]] | ||
+ | ** O WDTP é um provador de teoremas baseado no método de tablôs implementado por Wagner Dias. Na verdade, o WDTP é mais do que um provador de teoremas; é um arcabouço orientado a objetos (an object-oriented framework) para a implementação de métodos de prova baseados em tablôs. O arcabouço foi implementado em C++ e três métodos de tablôs foram implementados baseados neste arcabouço: os Tablôs Analíticos de Smullyan, os tablôs KE de Mondadori e D'Agostino's, e os tablôs KE-S3 de Finger e Wasserman. | ||
+ | |||
+ | ===== Baseados em Tablôs KE ===== | ||
+ | |||
+ | * [http://www.dainf.ct.utfpr.edu.br/~adolfo/KEMS/ KEMS - a KE-based Multi-Strategy theorem prover.] | ||
+ | ** "KEMS is a KE-based Multi-Strategy theorem prover. The KE system, a tableau method developed by Marco Mondadori and Marcello D'Agostino, was presented as an improvement, in the computational efficiency sense, over the Analytic Tableau method." |
Edição atual tal como 12h02min de 23 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 Analíticos
- jTAP - A Tableau Prover in Java
- "jTAP is a propositional tableau prover. It is implemented in Java and supports in its current version classical propositional logic, but it is easily extendable. The prover is described in the Unified Modeling Language (UML), an object-oriented modeling language. You can find some UML diagrams in the appendix of the jTAP documentation, which may help to understand the architecture of the prover and how it works."
- WDTP - Wagner Dias Tableau Prover
- O WDTP é um provador de teoremas baseado no método de tablôs implementado por Wagner Dias. Na verdade, o WDTP é mais do que um provador de teoremas; é um arcabouço orientado a objetos (an object-oriented framework) para a implementação de métodos de prova baseados em tablôs. O arcabouço foi implementado em C++ e três métodos de tablôs foram implementados baseados neste arcabouço: os Tablôs Analíticos de Smullyan, os tablôs KE de Mondadori e D'Agostino's, e os tablôs KE-S3 de Finger e Wasserman.
Baseados em Tablôs KE
- KEMS - a KE-based Multi-Strategy theorem prover.
- "KEMS is a KE-based Multi-Strategy theorem prover. The KE system, a tableau method developed by Marco Mondadori and Marcello D'Agostino, was presented as an improvement, in the computational efficiency sense, over the Analytic Tableau method."