WDTP - Wagner Dias Tableau Prover
(→Código-fonte) |
|||
| Linha 3: | Linha 3: | ||
O WDTP é um provador de teoremas baseado no método de tablôs implementado por [http://www.ime.usp.br/~dias/ Wagner Dias] durante seu mestrado em Ciência da Computação no [http://www.ime.usp.br/ IME-USP]. Seu orientador foi o professor [http://www.ime.usp.br/~mfinger/ Marcelo Finger]. | O WDTP é um provador de teoremas baseado no método de tablôs implementado por [http://www.ime.usp.br/~dias/ Wagner Dias] durante seu mestrado em Ciência da Computação no [http://www.ime.usp.br/ IME-USP]. Seu orientador foi o professor [http://www.ime.usp.br/~mfinger/ Marcelo Finger]. | ||
| − | A descrição do funcionamento do WDTP pode ser encontrada na Dissertação de Mestrado de Wagner Dias: [http://www.dainf.ct.utfpr.edu.br/~adolfo/etc/Software/WDTP/DissertacaoMestradoWagnerDias.pdf Implementação de Tableaux para Raciocínio por Aproximações], defendida em em 31 de outubro de 2002. Em nenhum lugar da dissertação ou do código o provador recebe um nome, portanto [[Adolfo Neto]] resolveu batizá-lo de WDTP (Wagner Dias Tableau Prover). | + | A descrição do funcionamento do WDTP pode ser encontrada na Dissertação de Mestrado de Wagner Dias: [http://www.dainf.ct.utfpr.edu.br/~adolfo/etc/Software/WDTP/DissertacaoMestradoWagnerDias.pdf Implementação de Tableaux para Raciocínio por Aproximações], defendida em em 31 de outubro de 2002. Em nenhum lugar da dissertação ou do código o provador recebe um nome, portanto [[Adolfo Neto]] resolveu batizá-lo de WDTP (Wagner Dias Tableau Prover). [[Adolfo Neto]], orientado pro Marcelo Finger, também fez, em 2003, algumas modificações neste provador que foram descritas no relatório [http://www.dainf.ct.utfpr.edu.br/~adolfo/etc/Software/WDTP/ModificationsWDTP_AdolfoNeto.pdf Modifications on the implementation of a framework for tableaux methods]. |
Edição de 11h58min de 23 de abril de 2009
Descrição
O WDTP é um provador de teoremas baseado no método de tablôs implementado por Wagner Dias durante seu mestrado em Ciência da Computação no IME-USP. Seu orientador foi o professor Marcelo Finger.
A descrição do funcionamento do WDTP pode ser encontrada na Dissertação de Mestrado de Wagner Dias: Implementação de Tableaux para Raciocínio por Aproximações, defendida em em 31 de outubro de 2002. Em nenhum lugar da dissertação ou do código o provador recebe um nome, portanto Adolfo Neto resolveu batizá-lo de WDTP (Wagner Dias Tableau Prover). Adolfo Neto, orientado pro Marcelo Finger, também fez, em 2003, algumas modificações neste provador que foram descritas no relatório Modifications on the implementation of a framework for tableaux methods.
Código-fonte
O código-fonte original do WDTP pode ser encontrado em http://www.ime.usp.br/~dias/project-tableau.tar.gz. O WDTP foi escrito em C++.
Em 23/04/2009, Adolfo Neto fez pequenas alterações deste código, criando duas novas versões:
- Versão do WDTP para Windows XP: esta versão foi compilada utilizando
- Versão do WDTP para Linux: Algumas adaptações foram feitas no código para que o projeto pudesse ser compilado com o gcc na versão "gcc version 4.3.2 (Ubuntu 4.3.2-1ubuntu12)"
Como executar
- Descompactar o pacote contendo o software
- Ir para o diretório criado pelo descompactador
- Executar um comando no formato "Usage: prove [-m analytic[+BU]*|ke[+V|P]|kes3[+PB]] [-v] -f %.prove|%.cnf"
