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

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 $\mathrm{\neg }p$ is the negation of $p$, which is true in an interpretation when $p$ is false in that interpretation, and $p\vee 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 $\text{false}\leftarrow a_1\wedge \mathrm{\dots }\wedge a_k$ is logically equivalent to $\mathrm{\neg }{a}_1\vee \mathrm{\dots }\vee \mathrm{\neg }{a}_k$.

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

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.

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.

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