Horn clause

A Horn clause is a clause (a disjunction of literals) with at most one positive, i.e. unnegated, literal.

Conversely, a disjunction of literals with at most one negated literal is called a dual-Horn clause.

A Horn clause with exactly one positive literal is a definite clause or a strict Horn clause;[2] a definite clause with no negative literals is sometimes called a unit clause,[3] and a unit clause without variables is sometimes called a fact;[4] and a Horn clause without a positive literal is sometimes called a goal clause (note that the empty clause consisting of no literals is a goal clause). These three kinds of Horn clauses are illustrated in the following propositional example:

In the non-propositional case, all variables[note 2] in a clause are implicitly universally quantified with the scope being the entire clause. Thus, for example:

¬ human(X) ∨ mortal(X)

stands for:

∀X( ¬ human(X) ∨ mortal(X) )

which is logically equivalent to:

∀X ( human(X) → mortal(X) )

Horn clauses are also the basis of logic programming, where it is common to write definite clauses in the form of an implication:

(p ∧ q ∧ ... ∧ t) → u

In fact, the resolution of a goal clause with a definite clause to produce a new goal clause is the basis of the SLD resolution inference rule, used to implement logic programming in the programming language Prolog.

In logic programming a definite clause behaves as a goal-reduction procedure. For example, the Horn clause written above behaves as the procedure:

to show u, show p and show q and ... and show t.

To emphasize this reverse use of the clause, it is often written in the reverse form:

u ← (p ∧ q ∧ ... ∧ t)

In Prolog this is written as:

u :- p, q, ..., t.

In logic programming and datalog, computation and query evaluation are performed by representing the negation of a problem to be solved as a goal clause. For example, the problem of solving the existentially quantified conjunction of positive literals:

∃X (p ∧ q ∧ ... ∧ t)

is represented by negating the problem (denying that it has a solution), and representing it in the logically equivalent form of a goal clause:

∀X (false ← p ∧ q ∧ ... ∧ t)

In Prolog this is written as:

:- p, q, ..., t.

Solving the problem amounts to deriving a contradiction, which is represented by the empty clause (or "false"). The solution of the problem is a substitution of terms for the variables in the goal clause, which can be extracted from the proof of contradiction. Used in this way, goal clauses are similar to conjunctive queries in relational databases, and Horn clause logic is equivalent in computational power to a universal Turing machine.

The Prolog notation is actually ambiguous, and the term “goal clause” is sometimes also used ambiguously. The variables in a goal clause can be read as universally or existentially quantified, and deriving “false” can be interpreted either as deriving a contradiction or as deriving a successful solution of the problem to be solved.

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 clauses D has a unique minimal model M. An atomic formula A is logically implied by D if and only if A is true in M. It follows that a problem P represented by an existentially quantified conjunction of positive literals is logically implied by D if and only if P is true in M. The minimal model semantics of Horn clauses is the basis for the stable model semantics of logic programs.[6]