Refinamentos para o método dos tableaux /

Abstract

No presente trabalho são propostos refinamentos sobre o método dos tableaux, tal como tradicionalmente apresentado, visando diminuir o número de nós das árvores de prova, bem como aumentar a possibilidade de obtenção de respostas. Para isto especificamos e implementamos três diferentes algoritmos baseados no método tradicional dos tableaux para a lógica clássica. O mais sofisticado e avançado dos três métodos recorre ao procedimento de unificação, comumente utilizado no método da resolução. Finalizamos este trabalho apresentando uma série de testes, para verificar experimentalmente a consecução dos objetivos propostos.