Horn Logic

Origin. Alfred Horn, "On sentences which are true of direct unions of algebras" (Journal of Symbolic Logic, 1951) — the clauses are named for a preservation theorem, not for a computational property, and the computational property was found twenty years later. Kowalski (1974) read Horn clauses as procedures; Dowling and Gallier (1984) gave the linear-time propositional algorithm.

Models. The fragment of first-order logic in which each clause has at most one positive literal. Written the other way round, that is a rule: A₁ ∧ ... ∧ Aₙ → B — a conclusion with conditions, and never a disjunctive conclusion. Everything tractable in logic programming, deductive databases, and description logic descends from that restriction, and everything it cannot say descends from it too.

Formalism.

Clauses: Definite: ¬A₁ ∨ ... ∨ ¬Aₙ ∨ B ≡ A₁ ∧ ... ∧ Aₙ → B (exactly one positive) Goal: ¬A₁ ∨ ... ∨ ¬Aₙ (no positive) Fact: B (n = 0) Horn = at most one positive literal.

Least model property: A set of definite clauses has a unique minimal Herbrand model. It is the least fixed point of the immediate-consequence operator T_P: T_P(I) = {B : A₁ ∧ ... ∧ Aₙ → B ∈ P, all Aᵢ ∈ I} lfp(T_P) = ⋃_n T_P^n(∅) — reached in ω steps, since T_P is continuous. Disjunction destroys this: p ∨ q has two minimal models and no least one.

Horn's theorem (1951): Universal Horn sentences are preserved under direct products. A class of algebras is a quasivariety iff it is axiomatized by universal Horn sentences. This is the original result and the reason for the name.

Complexity: Propositional HORNSAT: P-complete, decidable in linear time (Dowling–Gallier 1984). Full SAT: NP-complete. The restriction is exactly where the cliff is. First-order Horn: SLD-resolution is sound and complete; still undecidable, but the search is directed.

What it cannot say: No disjunctive conclusions: "p or q" is not Horn. No classical negation in the body: negation-as-failure is the substitute, and it is not classical. The least model property is what buys the tractability and what forces the non-classical negation.

Symbols.

Metatheory. The least model property is the whole subject: it makes "the meaning of a program" well defined, it makes bottom-up evaluation terminate, and it is exactly what disjunction destroys. Horn's 1951 preservation theorem and the 1984 linear-time algorithm are the same restriction found from opposite ends — model theory noticed that Horn sentences survive products, and complexity theory noticed they survive polynomial time, and the coincidence has never been explained beyond both following from the single positive literal. The fragment's descendants — Prolog, Datalog, the EL description logic, SMT theory solvers — are all cashing the same property.

Applies to. Logic programming and Prolog. Datalog and deductive databases. Tractable description logics — EL and its relatives are Horn fragments. Constraint logic programming. SMT, where Horn clauses are the standard verification-condition format. Quasivarieties in universal algebra.

Limitations. No disjunctive conclusions and no classical negation, which is most of what one wants to say. Negation-as-failure fills the gap and is not classical negation — it is nonmonotonic, and the stable-model and well-founded semantics exist because it has no obvious meaning. First-order Horn is still undecidable; the tractability is propositional. And the fragment is not closed under the operations one would want: the conjunction of two Horn theories is Horn, the disjunction is not.

© 2026 Lingenic LLC