Prova de Teoremas Utilizando Simplificação por Eliminação de Literais

O presente trabalho apresenta um método de prova de teoremas para lógica proposicional e de primeira ordem denominado Método de Simplificação por Eliminação de Literais (MSEL). O MSEL gera conclusões a a partir de fórmulas não clausais, como o método de Tableaux, evitando a geração de fórmulas redundantes que ocorre na conversão para forma clausal. Quando restringimos as fórmulas a cláusulas, o MSEL gera os mesmos resultados que a resolução, podendo utilizar as heurísticas tradicionais empregadas para contornar a complexidade da prova a partir de bases de conhecimento. Para o caso geral, são desenvolvidas heurísticas adicionais que procuram capturar a intenção do usuário, expressa na forma escolhida para apresentar as fórmulas.