Resolução com Claúsulas de Horn

O mecanismo de prova baseado na refutação por resolução é completo e correcto mas não é eficiente (na verdade é NP-completo).

Uma cláusula de Horn é uma cláusula que tem no máximo um literal positivo

• Exemplos:

Existem algoritmos de dedução baseados em cláusulas de Horn cuja complexidade temporal é linear.

• As linguagens Prolog e Mercury baseiam-se em cláusulas de Horn.