Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico. Programa de Pós-Graduação em Ciência da Computação. / Made available in DSpace on 2012-10-21T23:14:47Z (GMT). No. of bitstreams: 1 207778.pdf: 429850 bytes, checksum: 5a8ef0bdb25a1cedbc0312a1d037e76b (MD5) / Este trabalho desenvolve uma forma diferente de se obter árvores de prova por tablôs. Denominamos esse método de direto, por causa da característica em que a possível conclusão é inserida no tablô inicial, sem negá-la. Já o método dos tablôs por refutação se utiliza da negação da possível conclusão. No sistema de tablôs por prova direta para a lógica clássica, cada ramo está relacionado semanticamente à disjunção das fórmulas que o compõem, e o tablô completo corresponde semanticamente à conjunção de todas essas disjunções. Em qualquer um dos métodos baseados em tablôs para a Lógica Clássica, tanto direto quanto indireto, um ramo é considerado fechado se o mesmo contiver duas fórmulas contraditórias. No método direto o fechamento de um ramo corresponde à sua validade semântica, a qual implica, no caso do fechamento de todos os ramos, na validade da possível conclusão. Já no método indireto o fechamento de um ramo corresponde à insatisfatibilidade da negação da possível conclusão, o que por sua vez implica na validade da mesma.

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico. Programa de Pós-Graduação em Ciência da Computação. / Made available in DSpace on 2012-10-20T10:56:48Z (GMT). No. of bitstreams: 1 197133.pdf: 2644540 bytes, checksum: a258dbeabb2ac6818b4802500a65e309 (MD5) / Este trabalho tem como objetivo descrever o desenvolvimento de um provador de teoremas segundo o Método dos Tableaux. Para isso, foram propostos dois refinamentos com o intuito de tornar o método mais eficiente durante as etapas de prova. Esses refinamentos tratam da ordenação das fórmulas e da instanciação das variáveis, buscando diminuir a inserção de elementos na árvore, propiciando, assim, uma maior eficiência em relação ao número de nós. A linguagem Java foi utilizada para a implementação do provador, possibilitando a manipulação das fórmulas estruturadas como documentos XML. Ao final do trabalho, é verificada a eficiência do provador através da comparação com outros provadores em relação à sistematização das suas etapas de prova e dos resultados obtidos.