Provas de teoremas em lógica três-valorada

Abstract

Existem poucas ferramentas disponíveis atualmente capazes de avaliar fórmulas em Lógica Três-Valorada. Este trabalho teve como objetivo a codificação de um provador de teoremas para Lógica Três-Valorada usando a Tradução Bivalente e Resolução Clausal formulados em [1]. O provador foi submetido a uma série de testes de desempenho e comparado com outro provador construído em linguagem Prolog, o MUltseq [2]. Os desempenhos de ambos foram comparados tanto quanto ao tempo consumido quando ao uso de memória RAM. São apresentados os fundamentos da Lógica infinitamente-valorada de Łukasiewicz, as definições para a formulação da Lógica Três-Valorada, a definição de Tradução Bivalente e o método de Resolução Clausal. Em seguida, explica-se como foi feita a implementação do programa tradutor proposto, as ferramentas e programas utilizados, a saída esperada, a realização dos testes de comparação e, por fim, a verificação de um melhor desempenho e de um melhor uso de memória do provador construído em relação ao MUltseq.