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
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.
Last updated
