I am reading the Artificial Intelligence: A Modern Approach book and in the chapters about logic i noticed that in propositional logic the Modus ponens inference rule (used by the forward and backward chaining algorithms) requires the KB to be a conjunction of Horn clauses, while in first order logic the Generalized Modus ponens requires that the clauses are definite clauses.

The reason why it is like that is not explained anywhere. I would say that even in propositional logic we should consider only definite clauses because a goal clauses is like: Symbol1 Λ .. Λ Symboln => False and even if i can apply the Modus ponens rule i would add to the KB False which i don't think it's useful at all.

So does anyone know why there's that difference and we don't just use definite clauses in both cases?


Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.