Método dos Tableaux com Unificação

Letícia Carvalho Pivetta FendtArthur Ronald de Vallauris Buschbaum

In this work one refinement is proposed on the tableaux method, aiming to decrease the number of nodes of the proof trees, as well as to increase the possibility of obtaining answers. For this purpose a algorithm is specified, based on the traditional tableau method for classical logic, which appeals to the unification procedure, commonly used by the resolution method. Clique no link abaixo para buscar o texto completo deste trabalho na Web: Buscar na Web

Biblioteca Digital Brasileira de Computação - Contato:
     Mantida por: