Refutação por Resolução

A refutação por resolução é um mecanismo de inferência completo.

• Neste caso, usa-se a resolução para provar que a negação da consequência lógica é inconsistente com a premissa (meta-teorema da redução ao absurdo).

• No exemplo dado, prova-se que é inconsistente (basta mostrar que é possível derivar a fórmula 'Falso').

Passos da refutação por resolução:

• Converter a premissa e a negação da consequência lógica para um conjunto de cláusulas.

• Aplicar a resolução até obter a cláusula vazia.