WDTP - Wagner Dias Tableau Prover
Tabela de conteúdo |
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.
O WDTP é mais do que um provador de teoremas; é na verdade um arcabouço orientado a objetos (an object-oriented framework) para a implementação de métodos 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.
A descrição completa 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 por 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. O código-fonte destas modificações não está disponível.
Código-fonte
O código-fonte original do WDTP pode ser encontrado em http://www.ime.usp.br/~dias/project-tableau.tar.gz.
Em 23/04/2009, Adolfo Neto fez pequenas alterações neste código, criando duas novas versões:
- 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 seguinte versão: "gcc version 4.3.2 (Ubuntu 4.3.2-1ubuntu12)".
- Versão do WDTP para Windows XP: esta versão foi compilada utilizando MingW, uma versão do gcc (um compilador para C e C++) para Windows. A única diferença desta versão em relação à versão para Linux é que o tempo gasto para provar teoremas é medido apenas em segundos e não em milissegundos.
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"
Exemplos de execução
- Linha de comando:
prove -m analytic -f cases/gamma1.prove -v
- Saída:
0 T (a1|b1) 1 T (a1->(a2|b2)) 2 T (b1->(a2|b2)) 3 F (a2|b2) ------------------------------- 0 T (a1|b1) 1 T (a1->(a2|b2)) 2 T (b1->(a2|b2)) 3 F (a2|b2) 4 F a2 5 F b2 0 T a1 0 F a1 0 T (a2|b2) 0 F b1 0 T a2 0 T b2 0 T (a2|b2) 0 T a2 0 T b2 0 T b1 0 F a1 0 F b1 0 T (a2|b2) 0 T a2 0 T b2 0 T (a2|b2) 0 F b1 0 T (a2|b2) 0 T a2 0 T b2 x Total number of nodes: 21 Total number of formulae: 26 Elapsed time (s): 0.001298