Refutação por Resolução
Last updated
Last updated
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.