Horn Clause

A Horn clause is disjunctions of literals s.t. at most one literal is positive. It could also be written in implicative form which is commonly used in Formal Methods.

• Exactly one positive literal: definite clause (strict Horn clause) $p\wedge q\wedge \dots \to t$
• No positive literal: goal clause $p\wedge q\wedge \dots \to \mathtt{false}$

And a fact is when there’s no negative literal:

$$\mathtt{true}\to t$$

---

• Linear: A Horn clause is considered linear if its body contains at most one atom (or predicate). In the implication form, this means the conjunction on the left side has at most one term. Linear Horn clauses are generally easier to solve and analyze.
• A Horn clause is non-linear if its body contains more than one atom.

Complexity

The satisfiability of Propositional Horn Clauses (HORNSAT problem) is P-complete and solvable in linear time.

Related

• SAT : NP-complete