Definite clauses can be used in a proof by contradiction by allowing rules that give contradictions. For example, in the electrical wiring domain, it is useful to be able to specify that some prediction, such as that light $l_{2}$ is on, is not true. This will enable diagnostic reasoning to deduce that some switches, lights, or circuit breakers are broken.

## 5.6.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

 $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 $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}$.

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

###### Example 5.17.

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

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

The atom $c$ is false in all models of ${KB}_{1}$. To see this, suppose instead that $c$ is true in model $I$ of ${KB}_{1}$. Then $a$ and $b$ would both be true in $I$ (otherwise $I$ would not be a model of ${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 ${KB}_{1}$. Thus, $\neg c$ is true  in all models of ${KB}_{1}$, which can be written as

 ${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.18.

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

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

Either $c$ is false or $d$ is false in every model of ${KB}_{2}$. If they were both true in some model $I$ of ${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 ${KB}_{2}$. Similarly, either $c$ is false or $e$ is false in every model of ${KB}_{2}$. Thus

 ${KB}_{2}\models\neg c\vee\neg d$ ${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.19.

The set of clauses $\{a,false\leftarrow\mbox{}a\}$ is unsatisfiable. There is no interpretation that satisfies both clauses. Both $a$ and $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.

## 5.6.2 Assumables and Conflicts

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},\ldots,c_{r}\}$ is a conflict of ${KB}$ if

 ${KB}\cup\{c_{1},\ldots,c_{r}\}\models false.$

In this case, an answer is

 ${KB}\models\neg c_{1}\vee\ldots\vee\neg c_{r}.$

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

###### Example 5.20.

In Example 5.18, if $\{c,d,e,f,g,h\}$ is the set of assumables, then $\{c,d\}$ and $\{c,e\}$ are minimal conflicts of ${KB}_{2}$; $\{c,d,e,h\}$ is also a conflict, but not a minimal conflict.

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

## 5.6.3 Consistency-Based Diagnosis

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.

###### Example 5.21.

Consider the house wiring example depicted in Figure 5.2 and represented in Example 5.8. Figure 5.8 gives a background knowledge base suitable for consistency-based diagnosis. Normality assumptions, specifying that switches, circuit breakers, and lights must be ok to work as expected, are added to the clauses. There are no clauses for the $ok$ atoms, but they are made assumable.

The user is able to observe the switch positions and whether a light is lit or dark.

A light cannot be both lit and dark. This knowledge is stated in the following integrity constraints:

 $false\leftarrow\mbox{}{dark\_l}_{1}\wedge\mbox{}{lit\_l}_{1}.$ $false\leftarrow\mbox{}{dark\_l}_{2}\wedge\mbox{}{lit\_l}_{2}.$

Suppose the user observes that all three switches are up, and that $l_{1}$ and $l_{2}$ are both dark. This is represented by the atomic clauses

 $\begin{array}[]{lll}{{up\_s}_{1}.{}{}{}{}{}}&{{up\_s}_{2}.{}{}{}{}{}}&{{up\_s}% _{3}.}\\ {{dark\_l}_{1}.}&{{dark\_l}_{2}.}\end{array}$

Given the knowledge of Figure 5.8 together with the observations, there are two minimal conflicts:

 $\{{ok\_cb}_{1},{ok\_s}_{1},{ok\_s}_{2},{ok\_l}_{1}\}$ $\{{ok\_cb}_{1},{ok\_s}_{3},{ok\_l}_{2}\}.$

Thus, it follows that

 ${KB}\models\neg{ok\_cb}_{1}\vee\neg{ok\_s}_{1}\vee\neg{ok\_s}_{2}\vee\neg{ok\_% l}_{1}$ ${KB}\models\neg{ok\_cb}_{1}\vee\neg{ok\_s}_{3}\vee\neg{ok\_l}_{2}$

which means that at least one of the components $cb_{1}$, $s_{1}$, $s_{2}$, or $l_{1}$ must not be ok, and at least one of the components $cb_{1}$, $s_{3}$, or $l_{2}$ must not be ok.

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.

###### Example 5.22.

In Example 5.21, the disjunction of the negation of the two conflicts is a logical consequence of the clauses. Thus, the conjunction

 $(\neg{ok\_cb}_{1}\vee\neg{ok\_s}_{1}\vee\neg{ok\_s}_{2}\vee\neg{ok\_l}_{1})$ $\mbox{}\wedge\mbox{}(\neg{ok\_cb}_{1}\vee\neg{ok\_s}_{3}\vee\neg{ok\_l}_{2})$

follows from the knowledge base. This conjunction of disjunctions in conjunctive normal form (CNF) can be distributed into disjunctive normal form (DNF), a disjunction of conjunctions, here of negated atoms:

 $\neg{ok\_cb}_{1}\vee\mbox{}$ $(\neg{ok\_s}_{1}\wedge\mbox{}\neg{ok\_s}_{3})\vee(\neg{ok\_s}_{1}\wedge\mbox{}% \neg{ok\_l}_{2})\vee\mbox{}$ $(\neg{ok\_s}_{2}\wedge\mbox{}\neg{ok\_s}_{3})\vee(\neg{ok\_s}_{2}\wedge\mbox{}% \neg{ok\_l}_{2})\vee\mbox{}$ $(\neg{ok\_l}_{1}\wedge\mbox{}\neg{ok\_s}_{3})\vee(\neg{ok\_l}_{1}\wedge\mbox{}% \neg{ok\_l}_{2}).$

Thus, either $cb_{1}$ is broken or there is at least one of six double faults.

The propositions that are disjoined together correspond to the seven minimal diagnoses: $\{{ok\_cb}_{1}\}$, $\{{ok\_s}_{1},{ok\_s}_{3}\}$, $\{{ok\_s}_{1},{ok\_l}_{2}\}$, $\{{ok\_s}_{2},{ok\_s}_{3}\}$, $\{{ok\_s}_{2},{ok\_l}_{2}\}$, $\{{ok\_l}_{1},{ok\_s}_{3}\}$, $\{{ok\_l}_{1},{ok\_l}_{2}\}$. The system has proved that one of these combinations must be faulty.

## 5.6.4 Reasoning with Assumptions and Horn Clauses

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

### Bottom-Up Implementation

The bottom-up proof procedure for assumables and Horn clauses is an augmented version of the bottom-up algorithm for definite clauses presented in Section 5.3.2.

The modification to that algorithm is that the conclusions are pairs $\left$, where $a$ is an atom and $A$ is a set of assumables that imply $a$ in the context of the Horn clause knowledge base ${KB}$.

Initially, the conclusion set $C$ is $\{\left:a\hbox{ is assumable}\}$. Clauses can be used to derive new conclusions. If there is a clause $h\leftarrow\mbox{}b_{1}\wedge\mbox{}\ldots\wedge\mbox{}b_{m}$ such that for each $b_{i}$ there is some $A_{i}$ such that $\left\in C$, then $\left$ can be added to $C$. This covers the case of atomic clauses, with $m=0$, where $\left$ is added to $C$.

Figure 5.9 gives code for the algorithm. This algorithm is an assumption-based truth maintenance system (ATMS), and can be combined with the incremental addition of clauses and assumables.

When the pair $\left$ is generated, the assumptions $A$ form a conflict.

One refinement of this program is to prune supersets of assumptions. If $\left$ and $\left$ are in $C$, where $A_{1}\subset A_{2}$, then $\left$ can be removed from $C$ or not added to $C$. There is no reason to use the extra assumptions to imply $a$. Similarly, if $\left$ and $\left$ are in $C$, where $A_{1}\subseteq A_{2}$, then $\left$ can be removed from $C$ because $A_{1}$ and any superset – including $A_{2}$ – are inconsistent with the clauses given, and so nothing more can be learned from considering such sets of assumables.

###### Example 5.23.

Consider the axiomatization of Figure 5.8, discussed in Example 5.21.

Initially, in the algorithm of Figure 5.9, $C$ has the value

 $\{\left<{ok\_l}_{1},\{{ok\_l}_{1}\}\right>,\left<{ok\_l}_{2},\{{ok\_l}_{2}\}% \right>,\left<{ok\_s}_{1},\{{ok\_s}_{1}\}\right>,\left<{ok\_s}_{2},\{{ok\_s}_{% 2}\}\right>,$ $\left<{ok\_s}_{3},\{{ok\_s}_{3}\}\right>,\left<{ok\_cb}_{1},\{{ok\_cb}_{1}\}% \right>,\left<{ok\_cb}_{2},\{{ok\_cb}_{2}\}\right>\}.$

The following shows a sequence of values added to $C$ under one sequence of selections:

 ${\left<{live\_outside},\{\}\right>}$ ${\left<{live\_w}_{5},\{\}\right>}$ ${\left<{live\_w}_{3},\{{ok\_cb}_{1}\}\right>}$ ${\left<{up\_s}_{3},\{\}\right>}$ ${\left<{live\_w}_{4},\{{ok\_cb}_{1},{ok\_s}_{3}\}\right>}$ ${\left<{live\_l}_{2},\{{ok\_cb}_{1},{ok\_s}_{3}\}\right>}$ ${\left<{light\_l}_{2},\{\}\right>}$ ${\left<{lit\_l}_{2},\{{ok\_cb}_{1},{ok\_s}_{3},{ok\_l}_{2}\}\right>}$ ${\left<{dark\_l}_{2},\{\}\right>}$ ${\left.}$

Thus, the knowledge base entails

 $\neg{ok\_cb}_{1}\vee\neg{ok\_s}_{3}\vee\neg{ok\_l}_{2}.$

The other conflict can be found by continuing the algorithm.

### Top-Down Implementation

The top-down implementation is similar to the top-down definite-clause interpreter described in Figure 5.4, except the top-level query is to prove $false$, and the assumables encountered in a proof are not proved but collected.

The algorithm is shown in Figure 5.10. Different choices can lead to different conflicts being found. If no choices are available, the algorithm fails.

###### Example 5.24.

Consider the representation of the circuit in Example 5.21. The following is a sequence of the values of $G$ for one sequence of selections and choices that leads to a conflict:

 $\{false\}$ $\{{dark\_l}_{1},{lit\_l}_{1}\}$ $\{{lit\_l}_{1}\}$ $\{{light\_l}_{1},{live\_l}_{1},{ok\_l}_{1}\}$ $\{{live\_l}_{1},{ok\_l}_{1}\}$ $\{{live\_w}_{0},{ok\_l}_{1}\}$ $\{{live\_w}_{1},{up\_s}_{2},{ok\_s}_{2},{ok\_l}_{1}\}$ $\{{live\_w}_{3},{up\_s}_{1},{ok\_s}_{1},{up\_s}_{2},{ok\_s}_{2},{ok\_l}_{1}\}$ $\{{live\_w}_{5},{ok\_cb}_{1},{up\_s}_{1},{ok\_s}_{1},{up\_s}_{2},{ok\_s}_{2},{% ok\_l}_{1}\}$ $\{{live\_outside},{ok\_cb}_{1},{up\_s}_{1},{ok\_s}_{1},{up\_s}_{2},{ok\_s}_{2}% ,{ok\_l}_{1}\}$ $\{{ok\_cb}_{1},{up\_s}_{1},{ok\_s}_{1},{up\_s}_{2},{ok\_s}_{2},{ok\_l}_{1}\}$ $\{{ok\_cb}_{1},{ok\_s}_{1},{up\_s}_{2},{ok\_s}_{2},{ok\_l}_{1}\}$ $\{{ok\_cb}_{1},{ok\_s}_{1},{ok\_s}_{2},{ok\_l}_{1}\}.$

The set $\{{ok\_cb}_{1},{ok\_s}_{1},{ok\_s}_{2},{ok\_l}_{1}\}$ is returned as a conflict. Different choices of the clause to use can lead to another answer.