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 $\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 $false\leftarrow a_1\wedge \mathrm{\dots }\wedge a_k$ is logically equivalent to $\neg a_1\vee \mathrm{\dots }\vee \neg a_k$.

Unlike a definite-clause knowledge base, a Horn clause knowledge base can imply negations of atoms, as shown in Example 5.17.

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.

Reasoning from contradictions is a very useful tool. For many activities it is useful to know that some combination of assumptions is incompatible. For example, it is useful in planning to know that some combination of actions an agent is contemplating is impossible. When designing a new artifact, it is useful to know that some combination of components cannot work together.

In a diagnostic application it is useful to be able to prove that some components working normally is inconsistent with the observations of the system. Consider a system that has a description of how it is supposed to work and some observations. If the system does not work according to its specification, a diagnostic agent should identify which components could be faulty.

To carry out these tasks it is useful to be able to make assumptions that can be proven to be false.

An assumable is an atom that can be assumed in a proof by contradiction. A proof by contradiction derives a disjunction of the negation of assumables.

With a Horn clause knowledge base and explicit assumables, if the system can prove a contradiction from some assumptions, it can extract those combinations of assumptions that cannot all be true. Instead of proving a query, the system tries to prove $false$, and collects the assumables that are used in a proof.

If $KB$ is a set of Horn clauses, a conflict of $KB$ is a set of assumables that, given $KB$, implies $false$. That is, $C=\{c_1,\mathrm{\dots },c_r\}$ is a conflict of $KB$ if

In this case, an answer is

A minimal conflict is a conflict such that no strict subset is also a conflict.

In the examples that follow, assumables are specified using the assumable keyword followed by one or more assumable atoms separated by commas.

Making assumptions about what is working normally, and deriving what components could be abnormal, is the basis of consistency-based diagnosis. Suppose a fault is something that is wrong with a system. The aim of consistency-based diagnosis is to determine the possible faults based on a model of the system and observations of the system. By making the absence of faults assumable, conflicts can be used to prove what is wrong with the system.

Given the set of all conflicts, a user can determine what may be wrong with the system being diagnosed. However, sometimes it is more useful to give a disjunction of conjunctions of faults. This lets the user see whether all of the conflicts can be accounted for by a single fault or a pair of faults, or the system perhaps needs more faults.

Given a set of conflicts, a consistency-based diagnosis is a set of assumables that has at least one element in each conflict. A minimal diagnosis is a diagnosis such that no subset is also a diagnosis. For one of the diagnoses, all of its elements must be false in the world being modeled.

This section presents a bottom-up implementation and a top-down implementation for finding conflicts in Horn clause knowledge bases.