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?