Horn clauses

Horn clauses

To simplify our proof system, we can restrict the form or our logic sentences to a subset of all WFFs. This allows us to write more efficient algorithms, since they need only work with inputs of a restricted form. It also simplifies the language we use as programmers, and this makes it easier for us to write, reason about, and debug programs.

The restricted form we will use is what’s called a “Horn clause,” named after logician Alfred Horn, who was first to point out their significance and to describe their properties.

Recall that we refer to atoms and their negations as literals. A Horn clause is a disjunction of literals with at most one positive literal. The general form is

\begin{gather} H \lor \neg G_1 \lor \neg G_2 \lor \ldots \lor \neg G_n \end{gather}

Which is equivalent to

\begin{gather} H \lor \neg (G_1 \land G_2 \land \ldots \land G_n) \end{gather}

Now, consider the equivalence \neg A \lor B \equiv A \implies B. We may rewrite this B \lor \neg A \equiv B \Leftarrow A. We’re just reversing the order of terms. \lor is commutative, and in order to reverse the terms on the RHS, we have to change the direction of the implication, hence the left arrow \Leftarrow. We may read \Leftarrow as “is implied by.”

We can use this equivalence to rewrite (2) above, thus

\begin{gather} H \Leftarrow (G_1 \land G_2 \land \ldots \land G_n) \end{gather}

You may well ask why we choose the notation H and G here. To account for these choices, let’s consider three variations on the Horn clause.

\begin{gather} H \Leftarrow (G_1 \land G_2 \land \ldots \land G_n)\\ H \Leftarrow t\\ (G_1 \land G_2 \land \ldots \land G_n) \end{gather}

We call (4) a definite clause (Notice that (4) is identical with (3)). We call (5) a fact (sometimes called a unit clause). In this case, all the G_i are reduced to a single true literal. Of course, this may be (and often is) simplified to H, a bare assertion, without condition, and hence a fact. We call (6) a goal clause.

In Prolog, these are written a little differently.

(rule)  H :- G_1, G_2, ..., G_n.
(fact)  H.
(query) ?- G_1, G_2, ..., G_n.

The :- operator in Prolog is equivalent to \Leftarrow above. This is changed to ?- to indicate a query. Also, Prolog uses the comma to indicate logical and (\land). So these forms in Prolog are analogous to the three forms of Horn clauses. Generally, we build our knowledge base in Prolog using rules and facts, and then we query the system from a ?- prompt.

We call H the head, and we call the G_i the goals.

You may think that this subset of logic statements cannot be sufficient for our purposes. However, as it turns out Horn clauses are all we need for Turing-completeness!¹ So Horn clauses (and thus Prolog) are sufficient to express all possible calculations.

Turing machines and Horn clauses

A Turing machine is a tuple (Q, \Sigma, \Gamma, \delta, q_0, q_f), where Q is some set of states, \Sigma is the input alphabet not containing the blank symbol \square, \Gamma is the tape alphabet with \square \in \Gamma and \Sigma \subseteq \Gamma / \{\square\}, q_0 is the starting state, q_f is the final state, and \delta is the transition function which maps the current state and the symbol under the tape head to the next state, a symbol written at the current position, and some motion of the tape head left or right (L or R):

\begin{gather} \delta : Q \times \Gamma \rightarrow Q \times \Gamma \times \{L, R\} \end{gather}

How can we represent this with Horn clauses? Let the predicate T(l, q, r) be true if and only if q is the current state of the machine, l is the content of the tape which extends from the left of the tape head, and r is the content of the tape which extends from the tape head to the right. We may write xy to represent the concatenation of symbols x and y. Let a, b, c \in \Gamma, and let u, v \in \Gamma^* (where ^* is Kleene star). Suppose we have \delta(q_0, b) = (q_1, c, L). Then,

\begin{gather} (\forall u)(\forall v)(T(ua, q_0, bv) \implies T(u, q_1, acv)) \end{gather}

Treating universal quantification as implicit, this is a definite clause.

\begin{gather} T(ua, q_0, bv) \implies T(u, q_1, acv) \end{gather}

Likewise, suppose we have \delta(q_0, b) = (q_1, c, R). This can be expressed as

\begin{gather} T(ua, q_0, bv) \implies T(uac, q_1, v) \end{gather}

and it’s trivial to

\begin{gather} T(ua, q_0, bv) \implies T(uac, q_1, v) \end{gather}

Copyright © 2023–2025 Clayton Cafiero

No generative AI was used in producing this material. This was written the old-fashioned way.

Footnotes

1. These clauses are actually clauses of first-order predicate logic. It’s just that all variables in a such a clause are implicitly universally quantified with the scope being the entire clause.