1 Definition and syntax
A Horn clause is a logical formula that consists of a disjunction of literals with at most one positive literal. The general form is \( \lnot A_1 \lor \lnot A_2 \lor \dots \lor \lnot A_n \lor B \), where \( A_1, \dots, A_n \) (if any) are positive literals and \( B \) is either a positive literal or absent. The clause can be equivalently written as an implication: if \( n > 0 \), it is \( A_1 \land A_2 \land \dots \land A_n \Rightarrow B \); if \( n = 0 \) and \( B \) is present, the clause is simply \( B \), a fact.
1.1 Formal definition
In propositional logic, a Horn clause is a clause (a disjunction of literals) that contains at most one positive literal. In first-order logic, the definition is analogous: a clause with at most one positive literal, where literals are atomic formulas or their negations, and all variables are implicitly universally quantified. The positive literal is sometimes called the *head*, and the negative literals the *body*.
1.2 Types of Horn clauses
Three canonical types are distinguished based on the number of positive literals and the presence of negative literals.
1.2.1 Definite clauses
A definite clause contains exactly one positive literal. It represents a rule of the form “if all body literals are true, then the head is true.” In logic programming, definite clauses are the primary construct for encoding rules and facts (facts are definite clauses with an empty body).
1.2.2 Goal clauses
A goal clause contains no positive literal; it consists entirely of negative literals. It is written as \( \lnot A_1 \lor \lnot A_2 \lor \dots \lor \lnot A_n \) or, equivalently, as a query “? – \( A_1, A_2, \dots, A_n \)” in Prolog. A goal clause represents a statement to be proved false (i.e., it is a contradiction to be refuted).
1.2.3 Unit clauses
A unit clause is a clause consisting of a single literal. For Horn clauses, a unit clause is either a positive unit clause (a fact) or a negative unit clause (a denial). Positive unit clauses are a special case of definite clauses with an empty body.
1.3 Example in propositional logic
Consider the following set of propositional Horn clauses:
- \( p \) (positive unit clause)
- \( q \) (positive unit clause)
- \( \lnot p \lor \lnot q \lor r \) (definite clause: \( p \land q \Rightarrow r \))
- \( \lnot r \lor s \) (definite clause: \( r \Rightarrow s \))
- \( \lnot s \) (goal clause)
This set is unsatisfiable: from \( p \) and \( q \) we derive \( r \), then \( s \), which contradicts \( \lnot s \).
1.4 Example in first-order logic
A first-order Horn clause may contain variables. Example:
- \( \lnot \text{Father}(x, y) \lor \lnot \text{Father}(y, z) \lor \text{Grandfather}(x, z) \)
- \( \text{Father}(\text{John}, \text{Bob}) \)
- \( \text{Father}(\text{Bob}, \text{Ann}) \)
- \( \lnot \text{Grandfather}(\text{John}, \text{Ann}) \)
The first clause is definite, the next two are positive unit clauses, the last is a goal. The set is unsatisfiable because the facts imply the grandfather relationship.
2 Logical properties
Horn clauses possess distinctive logical properties that make them tractable for automated reasoning.
2.1 Semantics and models
The semantics of Horn clauses is typically given in terms of first-order interpretations, but two special model-theoretic notions are particularly relevant.
2.1.1 Minimal model semantics
A set of Horn clauses (especially definite clauses) always has a unique minimal model (with respect to set inclusion of true atoms). This model is the intersection of all models and corresponds to the least fixed point of an immediate consequence operator. In logic programming, the minimal model captures all logical consequences of the program.
2.1.2 Herbrand interpretations
For a first-order Horn clause set, the Herbrand universe (the set of all ground terms) and Herbrand base (the set of all ground atoms) provide a convenient domain. Herbrand models are interpretations where the domain is the Herbrand universe and each constant/function symbol is interpreted as itself. The minimal model of a Horn program is always a Herbrand model, which simplifies reasoning.
2.2 Relationship to Horn formulas
A Horn formula is a conjunction of Horn clauses. The class of Horn formulas is a strict subset of first-order logic. While arbitrary first-order formulas may be exponentially more complex, Horn formulas retain the property that their satisfiability can be decided in polynomial time (in propositional logic) and that they are closed under the formation of clauses.
2.3 Satisfiability and Horn-SAT
The propositional Horn satisfiability problem (Horn-SAT) asks whether a given conjunction of propositional Horn clauses has a satisfying assignment. It is one of the most well-known polynomial-time solvable variants of SAT.
2.3.1 Polynomial-time decidability
Horn-SAT is solvable in linear time (in the number of clause occurrences). The reason is that the implication form of Horn clauses allows efficient propagation: models can be built incrementally by setting variables true only when forced. This contrasts with general SAT, which is NP-complete.
2.3.2 Unit propagation algorithm
A straightforward algorithm for Horn-SAT is unit propagation: repeatedly identify unit clauses (clauses with a single literal) that must be satisfied. For a positive unit clause, set that variable to true and remove all clauses containing it positively; for a negative unit clause, set the variable to false and remove all clauses containing it negatively. This process continues until either a contradiction (empty clause) is derived or no more unit clauses remain. If any clause remains unsatisfied with all negative literals, the formula is unsatisfiable; otherwise, it is satisfiable.
3 Applications in computer science
Horn clauses are foundational in several areas of computer science, particularly where efficient deduction is required.
3.1 Logic programming
Logic programming languages, most notably Prolog, are based on Horn clauses. Programs consist of definite clauses (rules and facts), and queries are goal clauses.
3.1.1 Prolog and definite clause grammars
Prolog syntax writes definite clauses as Head :- Body1, Body2, ..., BodyN. Facts are written as Head. Queries are ?- Goal1, Goal2, .... Prolog’s execution is driven by SLD resolution. Definite clause grammars (DCGs) extend Horn clauses to parse natural language structures, using Horn clauses to represent grammar rules.
3.1.2 Query evaluation as SLD resolution
SLD resolution (Selective Linear Definite clause resolution) is the inference mechanism used in Prolog. Given a goal clause and a set of definite clauses, it repeatedly selects a literal from the goal, matches it with the head of a definite clause via unification, and replaces the literal with the body of that clause. This yields a linear derivation tree. Success occurs when the goal is reduced to the empty clause.
3.2 Automated theorem proving
Horn clauses are a fragment of first-order logic for which resolution is particularly efficient.
3.2.1 Horn clause resolution
Resolution for Horn clauses is refutation-complete and can be restricted to *linear input resolution* (resolving always with a clause from the input set). This is essentially the SLD resolution used in logic programming. The implication form allows an intuitive direction: from known facts (unit clauses) toward the goal.
3.2.2 Forward and backward chaining
Forward chaining starts from known facts (positive unit clauses) and applies definite clauses to derive new facts, continuing until the goal is reached or no new facts can be added. Backward chaining starts from the goal (represented as a negative literal) and works backwards, seeking clauses whose heads match the goal and recursively trying to satisfy their bodies. Both strategies are sound and complete for Horn clauses.
3.3 Knowledge representation
Horn clauses provide a natural way to represent declarative knowledge in rule-based systems.
3.3.1 Deductive databases
Deductive databases extend relational databases with rules expressed as Horn clauses. Facts correspond to base relations, and rules define derived relations. Queries are answered by evaluating Horn clause programs, often using bottom-up evaluation (e.g., semi-naive evaluation) that exploits the minimal model property.
3.3.2 Rule-based systems
Expert systems and production rule systems often use Horn-like rules: IF conditions THEN conclusion. These rules are essentially definite clauses. Efficient inference engines use forward or backward chaining over the rule set. The tractability of Horn clauses ensures that reasoning remains predictable and efficient for large knowledge bases.
4 Variants and generalizations
Over time, various extensions to Horn clauses have been studied to increase expressiveness while preserving some computational advantages.
4.1 Extended Horn clauses
Extended Horn clauses allow negated literals in the body of a clause, under certain restrictions (e.g., stratified negation). In logic programming, this corresponds to “normal” logic programs with negation as failure. The semantics becomes more complex (e.g., the stable model semantics), but the syntactic restriction still permits efficient reasoning for many practical cases.
4.2 Disjunctive Horn clauses
Disjunctive Horn clauses permit more than one positive literal (i.e., a disjunction of positive literals) while still requiring at most one positive literal in each clause? Actually, the term “disjunctive Horn clause” is sometimes used to describe clauses that are Horn except that the head may be a disjunction of several positive literals. This breaks the Horn property and generally increases complexity (satisfiability becomes NP-complete). Nevertheless, such clauses appear in disjunctive logic programming and answer set programming.
4.3 Horn clauses with equality
Adding equality to Horn clauses leads to the theory of Horn equational logic, where clauses may contain equations. This is the foundation of many algebraic specification languages and term rewriting systems. The satisfiability problem for Horn clauses with equality is still decidable in certain cases (e.g., for equational Horn theories with a finite Herbrand model) but can become undecidable in general due to the interaction of recursion and equality.