Inmathematical logic andlogic programming, aHorn clause is alogical formula of a particular rule-like form that gives it useful properties for use in logic programming,formal specification,universal algebra andmodel theory. Horn clauses are named for the logicianAlfred Horn, who first pointed out their significance in 1951.[1]
A Horn clause is a disjunctiveclause (adisjunction ofliterals) with at most one positive, i.e.unnegated, literal.
Conversely, a disjunction of literals with at most one negated literal is called adual-Horn clause.
A Horn clause with exactly one positive literal is adefinite clause or astrict Horn clause;[2] a definite clause with no negative literals is aunit clause,[3] and a unit clause without variables is afact;[4]a Horn clause without a positive literal is agoal clause.The empty clause, consisting of no literals (which is equivalent tofalse), is a goal clause.These three kinds of Horn clauses are illustrated in the followingpropositional example:
| Type of Horn clause | Disjunction form | Implication form | Read intuitively as |
|---|---|---|---|
| Definite clause | ¬p ∨ ¬q ∨ ... ∨ ¬t ∨u | u ← (p ∧q ∧ ... ∧t) | assume that, ifp andq and ... andt all hold, then alsou holds |
| Fact | u | u ←true | assume that u holds |
| Goal clause | ¬p ∨ ¬q ∨ ... ∨ ¬t | false ← (p ∧q ∧ ... ∧t) | show that p andq and ... andt all hold[5] |
All variables in a clause are implicitlyuniversally quantified with the scope being the entire clause. Thus, for example:
stands for:
which is logically equivalent to:
Horn clauses play a basic role inconstructive logic andcomputational logic. They are important inautomated theorem proving byfirst-order resolution, because theresolvent of two Horn clauses is itself a Horn clause, and the resolvent of a goal clause and a definite clause is a goal clause. These properties of Horn clauses can lead to greater efficiency of proving a theorem: the goal clause is the negation of this theorem; seeGoal clause in the above table. Intuitively, if we wish to prove φ, we assume ¬φ (the goal) and check whether such assumption leads to a contradiction. If so, then φ must hold. This way, a mechanical proving tool needs to maintain only one set of formulas (assumptions), rather than two sets (assumptions and (sub)goals).
Propositional Horn clauses are also of interest incomputational complexity. The problem of finding truth-value assignments to make a conjunction of propositional Horn clauses true is known asHORNSAT. This problem isP-complete and solvable inlinear time.[6] In contrast, the unrestrictedBoolean satisfiability problem is anNP-complete problem.
Inuniversal algebra, definite Horn clauses are generally calledquasi-identities; classes of algebras definable by a set of quasi-identities are calledquasivarieties and enjoy some of the good properties of the more restrictive notion of avariety, i.e., an equational class.[7] From the model-theoretical point of view, Horn sentences are important since they are exactly (up to logical equivalence) those sentences preserved underreduced products; in particular, they are preserved underdirect products. On the other hand, there are sentences that are not Horn but are nevertheless preserved under arbitrary direct products.[8]
Horn clauses are also the basis oflogic programming, where it is common to write definite clauses in the form of animplication:
In fact, the resolution of a goal clause with a definite clause to produce a new goal clause is the basis of theSLD resolution inference rule, used in implementation of the logic programming languageProlog.
In logic programming, a definite clause behaves as a goal-reduction procedure. For example, the Horn clause written above behaves as the procedure:
To emphasize this reverse use of the clause, it is often written in the reverse form:
InProlog this is written as:
u:-p,q,...,t.
In logic programming, a goal clause, which has the logical form
represents the negation of a problem to be solved. The problem itself is an existentially quantified conjunction of positive literals:
The Prolog notation does not have explicit quantifiers and is written in the form:
:-p,q,...,t.
This notation is ambiguous in the sense that it can be read either as a statement of the problem or as a statement of the denial of the problem. However, both readings are correct. In both cases, solving the problem amounts to deriving the empty clause. In Prolog notation this is equivalent to deriving:
:-true.
If the top-level goal clause is read as the denial of the problem, then the empty clause representsfalse and the proof of the empty clause is a refutation of the denial of the problem. If the top-level goal clause is read as the problem itself, then the empty clause representstrue, and the proof of the empty clause is a proof that the problem has a solution.
The solution of the problem is a substitution of terms for the variablesX in the top-level goal clause, which can be extracted from the resolution proof. Used in this way, goal clauses are similar toconjunctive queries inrelational databases, and Horn clause logic is equivalent in computational power to auniversal Turing machine.
Van Emden and Kowalski (1976) investigated the model-theoretic properties of Horn clauses in the context of logic programming, showing that every set of definite clausesD has a unique minimal modelM. Anatomic formulaA is logically implied byD if and only ifA is true inM. It follows that a problemP represented by an existentially quantified conjunction of positive literals is logically implied byD if and only ifP is true inM. The minimal model semantics of Horn clauses is the basis for thestable model semantics of logic programs.[9]
