Horn Clause

A Horn clause is a disjunctive clause having at most one positive literal. Horn clauses are useful in speeding up the boolean satisfiability problem (SAT).

Definition §

Horn Clause

A Horn clause, $H$, is a disjunctive clause with at most one positive literal. That is, it either consists entirely of negations, or has one positive literal:

$$H=(\neg P_1,\neg P_2,\dots )\text{ or }H=(\neg P_1,\neg P_2,\dots Q)$$

If it contains exactly one positive literal, it is a definite clause and can be expressed as an implication:

$$H=(P_1\wedge P_2\wedge \dots )\to Q$$

Also note that a unit clause (one atom) is also a Horn clause, which can be expressed using propositional logic equivalences:

$$P\equiv (\top \to P)\neg P\equiv (P\to \perp )$$

Propositional Logic §

Propositional Horn clauses can be used to