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 definite universal Horn sentences (quasi-identities). 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 yields the tractability and what forces the non-classical negation.

Symbols.

Symbol	Unicode	Name	Meaning
←	U+2190	Leftwards arrow / Rule	B ← A₁, ..., Aₙ (Prolog notation)
→	U+2192	Rightwards arrow / Implication	The same rule written forwards
¬	U+00AC	Not sign / Negation	Marks the negative literals of a clause
∨	U+2228	Logical or / Disjunction	Clause form; at most one disjunct may be positive
∧	U+2227	Logical and / Conjunction	Joins the conditions of a rule body
≡	U+2261	Identical to	Logical equivalence of the two clause notations
T_P	—	Consequence operator	Immediate consequences of the program P
lfp	—	Least fixed point	The minimal Herbrand model, ⋃ₙ T_Pⁿ(∅)
⋃	U+22C3	N-ary union	The union of the iterates of T_P
∅	U+2205	Empty set	The starting interpretation of the iteration
∈	U+2208	Element of	Membership in a program or an interpretation
ω	U+03C9	Small letter omega	The ordinal at which the iteration closes
⊨	U+22A8	True / Entailment	Consequence over the least model
A, B	—	Atoms	Positive literals; A in bodies, B in heads
P	—	Program	A finite set of definite clauses
SLD	—	Selective Linear Definite resolution	The goal-directed proof procedure

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 — all rest on 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.