WDTP - Wagner Dias Tableau Prover

De Wiki DAINF
(Diferença entre revisões)
(→Descrição)
Linha 1: Linha 1:
 
== Descrição ==
 
== Descrição ==
  
−
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 é 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 '''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].  
  
−
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  
+
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.
−
os tablôs KE-S3 de Finger e Wasserman.
+
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 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.  
+
A descrição completa 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].
+
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 [http://www.dainf.ct.utfpr.edu.br/~adolfo/etc/Software/WDTP/ModificationsWDTP_AdolfoNeto.pdf 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 ==
 
== 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 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:
+
Em 23/04/2009, [[Adolfo Neto]] fez pequenas alterações neste código, criando duas novas versões:
−
* [http://www.dainf.ct.utfpr.edu.br/~adolfo/etc/Software/WDTP/ProjectTableauWindows.zip Versão do WDTP para Windows XP]: esta versão foi compilada utilizando
+
* [http://www.dainf.ct.utfpr.edu.br/~adolfo/etc/Software/WDTP/project-tableau-linux.zip 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)".
−
* [http://www.dainf.ct.utfpr.edu.br/~adolfo/etc/Software/WDTP/project-tableau-linux.zip 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)"
+
* [http://www.dainf.ct.utfpr.edu.br/~adolfo/etc/Software/WDTP/ProjectTableauWindows.zip Versão do WDTP para Windows XP]: esta versão foi compilada utilizando [http://www.mingw.org/ MingW], uma versão do [http://gcc.gnu.org/ 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.
  
  
Linha 25: Linha 24:
 
# Ir para o diretório criado pelo descompactador
 
# 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"
 
# 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:
 +
<pre>
 +
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
 +
</pre>

Edição de 12h17min de 23 de abril de 2009

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

  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"

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
Obtida de "http://dainf.ct.utfpr.edu.br/wiki/index.php?title=WDTP_-_Wagner_Dias_Tableau_Prover&oldid=1452"
Ferramentas pessoais