WDTP: Provador de teoremas baseado em tablôs analíticos, KE e KE-S3 de Wagner Dias e Marcelo Finger

Em 2002, Wagner Dias, aluno de mestrado do Marcelo Finger no IME-USP, implementou um provador de teoremas baseado em tablôs analíticos, tablôs KE e tablôs KE-S3. Eu batizei este provador de WDTP (Wagner Dias Tableau Prover).

O código-fonte original está disponível na página do Wagner Dias: http://www.ime.usp.br/~dias/. Ontem, ao tentar compilar com a versão do gcc instalado na minha máquina, não consegui e resolvi fazer as modificações necessárias no código para que ele pudesse rodar tanto no meu Linux Ubuntu 8.10 com gcc 4.3.2 quanto no meu Windows XP rodando MingW 3.4.2.

As novas versões estão disponíveis em:

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

Mais informações sobre o WDTP (incluindo a Dissertação de Mestrado do Wagner Dias) estão em http://www.dainf.ct.utfpr.edu.br/wiki/index.php/WDTP_-_Wagner_Dias_Tableau_Prover

Acredito que este programa pode ser útil para os que lecionam lógica para estudantes de computação, pois ele gera provas (em formato texto) de sequentes. Por exemplo, a prova abaixo é do sequente Gamma1 ( a1|b1, a1->(a2|b2), b1->(a2|b2) |- a2|b2 )  usando o método dos tablôs analíticos:

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
   

Não conheço nenhum outro provador baseado no método de tablôs analíticos que gere a árvore de prova. Se alguém conhecer, peço que me avise.