WDTP - Wagner Dias Tableau Prover

De Wiki DAINF
Edição feita às 12h03min de 23 de abril de 2009 por Adolfo (disc | contribs)

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.

Este framework foi implementado em C++ e três métodos de tablôs foram implementados: 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 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:


Como executar

  1. Descompactar o pacote contendo o software
  2. Ir para o diretório criado pelo descompactador
  3. Executar um comando no formato "Usage: prove [-m analytic[+BU]*|ke[+V|P]|kes3[+PB]] [-v] -f %.prove|%.cnf"
Ferramentas pessoais