Horn clause

A Horn clause is a logical disjunction of literals, where at most one of the literals is positive, and all others are negative. It is named after Alfred Horn, who first described them in a 1951 article.

A Horn clause with exactly one positive literal is known as a definite clause. If a definite clause has no negative literals, it is sometimes referred to as a "fact." Conversely, a Horn clause without any positive literals is often called a goal clause.These three kinds of Horn clauses are shown in the following propositional example:

definite clause: $\neg p\lor \neg q\vee \cdots \vee \neg t\vee u$

is an example of a definite Horn clause. Here's how to interpret it:

Breakdown of the Clause

• Negated Literals (¬p,¬q,…,¬t): These are the negative literals in the clause. Each represents a condition that must not be true.
• Positive Literal (u): This is the single positive literal in the clause. It represents the conclusion or outcome that holds if all the negated conditions are met.

Explanation

A definite Horn clause has exactly one positive literal and one or more negative literals. In this case, u is the positive literal, and ¬p,¬q,…,¬t are the negative literals.

The interpretation of the clause is:

• If p is false, q is false, ..., and t is false, then u must be true.
• Alternatively, it can be seen as a logical implication: if p, q, ..., and t are all true, then u must be true. This is because ¬p∨¬q∨...∨¬t∨u is logically equivalent to the implication (p∧q∧⋯∧t)→u.

fact: $u$

is a fact horn clause

Explanation

• In this case, p is a positive literal, and there are no negative literals.
• This clause asserts that p is simply true, without any conditions. Since there are no negative literals, it doesn’t depend on any other conditions—it’s just a fact.

In logic programming (like in Prolog), such a clause represents a basic truth or known fact in the system.

goal clause: $\neg p\lor \neg q\vee \cdots \vee \neg t$

Goal Horn Clause

A goal Horn clause is a Horn clause that has no positive literals, only negative ones.

Example

$\neg p\lor \neg q\vee \cdots \vee \neg t$

Explanation

• In this case, all literals p, q, ..., t are negated, and there is no positive literal.
• This type of clause is often used to represent a goal or query that needs to be satisfied.
• It can be interpreted as asking the system whether all the conditions p, q, ..., t can be false at the same time. If so, the goal is achieved.

In logic programming, a goal clause is used to specify what the system should prove or satisfy based on the given facts and rules.

In the non-propositional case, all variables in a clause are implicitly universally quantified within scope the entire clause. Thus, for example:

$\neg {\text{human}}(X)\lor {\text{mortal}}(X)$

stands for:

$\forall X(\neg {\text{human}}(X)\lor {\text{mortal}}(X))$

which is logically equivalent to:

$\forall X({\text{human}}(X)\rightarrow {\text{mortal}}(X)).$

Horn clauses play a basic role in constructive logic and computational logic. They are important in automated theorem proving by first-order resolution because the resolvent 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 efficiencies in proving a theorem (represented as the negation of a goal clause).

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

$(p\wedge q\wedge \cdots \wedge t)\rightarrow 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 and 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 $\cdots$ and show $t$.

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

$u\leftarrow (p\land q\land \cdots \land t)$

In Prolog this is written as:

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

However, the Prolog notation is unclear, and the term “goal clause” is sometimes also used differently. 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.

Propositional Horn clauses are also of interest in computational complexity, where the problem of finding truth value assignments to make a conjunction of propositional Horn clauses true is a P-complete problem (in fact solvable in linear time ), sometimes called HORNSAT. (The unrestricted Boolean satisfiability problem is an NP-complete problem however.) Satisfiability of first-order Horn clauses is undecidable.

Bibliography

• Alfred Horn (1951), "On sentences which are true of direct unions of algebras", Journal of Symbolic Logic, 16, 14–21.
• Dowling, W. and Gallier, J. (1984), "Linear-time algorithms for testing the satisfiability of propositional Horn formulae". Journal of Logic Programming, 3, 267–284.
• M. van Emden and R. Kowalski [1976] The semantics of predicate logic as a programming language. Journal of ACM, Vol. 23, 733–742.