WDTP - Wagner Dias Tableau Prover
(→Como executar) |
(→Como executar) |
||
(15 edições intermediárias de 2 usuários não apresentadas) | |||
Linha 3: | Linha 3: | ||
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''' é 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 de prova baseados em tablôs. | + | 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. |
− | 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 <tt>"-v"</tt>) 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: [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. | ||
Linha 16: | Linha 17: | ||
Em 23/04/2009, [[Adolfo Neto]] fez pequenas alterações neste 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/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 seguinte 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. | + | * [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] 3.4.2, 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. |
== Como executar == | == Como executar == | ||
Linha 22: | Linha 23: | ||
# Descompactar o pacote contendo o software | # Descompactar o pacote contendo o software | ||
# Ir para o diretório criado pelo descompactador | # Ir para o diretório criado pelo descompactador | ||
− | # Executar um comando no formato <tt>"prove [-m analytic[+BU]*|ke[+V|P]|kes3[+PB]] [-v] -f %.prove|%.cnf"</tt> | + | # Dar o comando <tt>make clean</tt> |
+ | # Dar o comando <tt>make all</tt> | ||
+ | # Executar um comando no formato <tt>"./prove [-m analytic[+BU]*|ke[+V|P]|kes3[+PB]] [-v] -f %.prove|%.cnf"</tt> | ||
=== Exemplos de execução === | === Exemplos de execução === | ||
+ | No diretório <tt>cases</tt> 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 <tt>cases</tt>, 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 no seguinte formato: | ||
+ | <pre> | ||
+ | T (a1|b1) | ||
+ | T (a1->(a2|b2)) | ||
+ | T (b1->(a2|b2)) | ||
+ | F (a2|b2) | ||
+ | </pre> | ||
+ | |||
+ | Observe que: | ||
+ | * as premissas recebem um marca T; | ||
+ | * a conclusão recebe uma marca 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: | * Linha de comando: | ||
<tt>prove -m analytic -f cases/gamma1.prove -v</tt> | <tt>prove -m analytic -f cases/gamma1.prove -v</tt> | ||
Linha 68: | Linha 96: | ||
Total number of formulae: 26 | Total number of formulae: 26 | ||
Elapsed time (s): 0.001298 | Elapsed time (s): 0.001298 | ||
+ | </pre> | ||
+ | |||
+ | ==== Exemplo 2: Gamma1 com tablôs KE ==== | ||
+ | * Linha de comando: | ||
+ | <tt>prove -m analytic -f cases/gamma1.prove -v</tt> | ||
+ | * 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 | ||
+ | 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 | ||
</pre> | </pre> |
Edição atual tal como 14h58min de 16 de setembro de 2011
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 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
- Descompactar o pacote contendo o software
- Ir para o diretório criado pelo descompactador
- Dar o comando make clean
- Dar o comando make all
- 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 no seguinte formato:
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 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:
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