What is the advantage of Horn logic in comparision to predicate logic or proposition logic

Question

Can anybody explain with an example what the advantage of horn logic in comparison with predicate and proposition logic is?

Answer 1

See :

• Michael Huth and Mark Ryan, Logic in Computer Science : Modelling and Reasoning about Systems, Cambridge UP (2nd ed 2004) :1.5.3 Horn clauses and satisfiability (page 65) :

We have already commented on the computational price we pay for transforming a propositional logic formula into an equivalent CNF. The latter class of formulas has an easy syntactic check for validity, but its test for satisfiability is very hard in general.

Fortunately, there are practically important subclasses of formulas which have much more efficient ways of deciding their satisfiability. One such example is the class of Horn formulas.

Answer 2

Horn logic is a subset of propositional and predicate logic where all statements are in a special format so that you can have very fast computer algorithms to test for satisfiability (and, as such, logical consequence).

But this only works because of the format of the statements, and in general, not all statements of propositional and predicate logic can be put into that format ... which is why Horn logic is a subset.