WDTP - Wagner Dias Tableau Prover - Histórico de revisão

Adolfo: /* Como executar */

2011-09-16T17:58:21Z

Como executar

Adolfo em 21h08min de 1 de abril de 2011

2011-04-01T21:08:14Z

Ceutotal: /* Descrição */

2011-01-10T10:17:09Z

Descrição

Adolfo: /* Exemplos de execução */

2009-07-05T17:54:52Z

Exemplos de execução

Adolfo: /* Exemplos de execução */

2009-04-23T14:51:58Z

Exemplos de execução

Adolfo: /* Exemplos de execução */

2009-04-23T14:50:41Z

Exemplos de execução

Adolfo: /* Exemplos de execução */

2009-04-23T14:50:19Z

Exemplos de execução

Adolfo: /* Exemplos de execução */

2009-04-23T14:47:13Z

Exemplos de execução

Adolfo: /* Código-fonte */

2009-04-23T14:36:30Z

Código-fonte

Adolfo: /* Descrição */

2009-04-23T14:26:01Z

Descrição

@@ Linha 23: / Linha 23: @@
 # Descompactar o pacote contendo o software
 # 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>
 === Exemplos de execução ===

@@ Linha 9: / Linha 9: @@
 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 por Marcelo Finger [[http://www.inpresso.com.br/loja/ Cartões de Visita]], 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.
+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 ==

@@ Linha 9: / Linha 9: @@
 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 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.
+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 [[http://www.inpresso.com.br/loja/ Cartões de Visita]], 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 ==

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

@@ Linha 36: / Linha 36: @@
 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:
+deve ser escrito num arquivo no seguinte formato:
 <pre>
 T (a1|b1)

@@ Linha 28: / Linha 28: @@
 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 cases, onde:
+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");

@@ Linha 33: / Linha 33: @@
 * "&" é a "conjunção" ("e");
 * "->" é a "implicação" ("se então").
 ==== Exemplo 1: Gamma1 com tablôs analíticos ====

← Versão anterior		Edição de 14h47min de 23 de abril de 2009
Linha 26:		Linha 26:

	=== 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 cases, onde:
		+	* "!" é a "negação";
		+	* "\|" é a "disjunção" ("ou");
		+	* "&" é a "conjunção" ("e");
		+	* "->" é a "implicação" ("se então").

	==== Exemplo 1: Gamma1 com tablôs analíticos ====		==== Exemplo 1: Gamma1 com tablôs analíticos ====

@@ Linha 17: / Linha 17: @@
 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/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 ==

@@ Linha 5: / Linha 5: @@
 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 interessantes do WDTP é imprimir (usando a opção <tt>"-v"</tt>) as provas completas obtidas pelo provador (ver a seção "Exemplos de execução" abaixo).
+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.