# 5.5.1 Horn Clauses

The definite clause language does not allow a contradiction to be stated. However, a simple expansion of the language can allow proof by contradiction.

An integrity constraint is a clause of the form

 $\displaystyle{\mbox{false}\leftarrow\mbox{}a_{1}\wedge\mbox{}\ldots\wedge\mbox% {}a_{k}.}$

where the $a_{i}$ are atoms and false is a special atom that is false in all interpretations.

A Horn clause is either a definite clause or an integrity constraint. That is, a Horn clause has either false or a normal atom as its head.

Integrity constraints allow the system to prove that some conjunction of atoms is false in all models of a knowledge base. Recall that $\neg p$ is the negation of $p$, which is true in an interpretation when $p$ is false in that interpretation, and $p\vee\mbox{}q$ is the disjunction of $p$ and $q$, which is true in an interpretation if $p$ is true or $q$ is true or both are true in the interpretation. The integrity constraint $\mbox{false}\leftarrow\mbox{}a_{1}\wedge\mbox{}\ldots\wedge\mbox{}a_{k}$ is logically equivalent to $\neg a_{1}\vee\mbox{}\ldots\vee\mbox{}\neg a_{k}$.

A Horn clause knowledge base can imply negations of atoms, as shown in Example 5.19.

###### Example 5.19.

Consider the knowledge base $\mbox{KB}_{1}$:

 $\displaystyle{\mbox{false}\leftarrow\mbox{}a\wedge\mbox{}b.}$ $\displaystyle{a\leftarrow\mbox{}c.}$ $\displaystyle{b\leftarrow\mbox{}c.}$

The atom $c$ is false in all models of $\mbox{KB}_{1}$. To see this, suppose instead that $c$ is true in model $I$ of $\mbox{KB}_{1}$. Then $a$ and $b$ would both be true in $I$ (otherwise $I$ would not be a model of $\mbox{KB}_{1}$). Because false is false in $I$ and $a$ and $b$ are true in $I$, the first clause is false in $I$, a contradiction to $I$ being a model of $\mbox{KB}_{1}$. Thus $\neg c$ is true in all models of $\mbox{KB}_{1}$, which can be written as

 $\displaystyle{\mbox{KB}_{1}\models\neg c}$

Although the language of Horn clauses does not allow disjunctions and negations to be input, disjunctions of negations of atoms can be derived, as the following example shows.

###### Example 5.20.

Consider the knowledge base $\mbox{KB}_{2}$:

 $\displaystyle{\mbox{false}\leftarrow\mbox{}a\wedge\mbox{}b.}$ $\displaystyle{a\leftarrow\mbox{}c.}$ $\displaystyle{b\leftarrow\mbox{}d.}$ $\displaystyle{b\leftarrow\mbox{}e.}$

Either $c$ is false or $d$ is false in every model of $\mbox{KB}_{2}$. If they were both true in some model $I$ of $\mbox{KB}_{2}$, both $a$ and $b$ would be true in $I$, so the first clause would be false in $I$, a contradiction to $I$ being a model of $\mbox{KB}_{2}$. Similarly, either $c$ is false or $e$ is false in every model of $\mbox{KB}_{2}$. Thus,

 $\displaystyle{\mbox{KB}_{2}\models\neg c\vee\neg d}$ $\displaystyle{\mbox{KB}_{2}\models\neg c\vee\neg e.}$

A set of clauses is unsatisfiable if it has no models. A set of clauses is provably inconsistent with respect to a proof procedure if false can be derived from the clauses using that proof procedure. If a proof procedure is sound and complete, a set of clauses is provably inconsistent if and only if it is unsatisfiable.

It is always possible to find a model for a set of definite clauses. The interpretation with all atoms true is a model of any set of definite clauses. Thus, a definite-clause knowledge base is always satisfiable. However, a set of Horn clauses can be unsatisfiable.

###### Example 5.21.

The set of clauses $\{a,\mbox{false}\leftarrow\mbox{}a\}$ is unsatisfiable. There is no interpretation that satisfies both clauses. Both $a$ and $\mbox{false}\leftarrow\mbox{}a$ cannot be true in any interpretation.

Both the top-down and the bottom-up proof procedures can be used to prove inconsistency, by using false as the query.