WDTP - Wagner Dias Tableau Prover

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 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.

Uma das características mais interessantes do WDTP é permitir ao usuário (usando a opção "-v") imprimir a árvore de prova completa obtida pelo provador (ver a seção "Exemplos de execução" abaixo).

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 (em C++) 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 3.4.2, 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

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

Exemplos de execução

No diretório cases já existem vários problemas que podem ser usados para testar o provador. Para criar um novo problema, basta seguir a sintaxe dos problemas disponíveis em cases, onde:

• "!" é a "negação";
• "|" é a "disjunção" ("ou");
• "&" é a "conjunção" ("e");
• "->" é a "implicação" ("se então").

Por exemplo, o problema Gamma1, que é descrito pelo sequente:

• a1|b1, a1->(a2|b2), b1->(a2|b2) |- a2|b2

deve ser escrito num arquivo da seguinte forma:

T (a1|b1)
T (a1->(a2|b2))
T (b1->(a2|b2))
F (a2|b2)

Observe que:

• as premissas recebem um marca T</>;
• a conclusão recebe uma marca <tt>F</>;
• todas as fórmulas são totalmente "parentizadas", isto é, têm todos os parênteses necessários.

Exemplo 1: Gamma1 com tablôs analíticos

• Linha de comando:

<tt>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

Exemplo 2: Gamma1 com tablôs KE

• 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
  1 T (a2|b2)
  2 T b2
  0 F a1
  1 T b1
  2 T (a2|b2)
  3 T b2
x

Total number of nodes:    3
Total number of formulae: 13
Elapsed time (s):         0.000525