5.6 Proving by Contradiction

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 l2 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


where the ai 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 ¬p is the negation of p, which is true in an interpretation when p is false in that interpretation, and pq 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 falsea1ak is logically equivalent to ¬a1¬ak.

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 KB1:


The atom c is false in all models of KB1. To see this, suppose instead that c is true in model I of KB1. Then a and b would both be true in I (otherwise I would not be a model of KB1). 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 KB1. Thus, ¬c is true  in all models of KB1, which can be written as


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 KB2:


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


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,falsea} is unsatisfiable. There is no interpretation that satisfies both clauses. Both a and falsea 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={c1,,cr} 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.

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 KB2; {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:

Figure 5.8: Knowledge for Example 5.21

Suppose the user observes that all three switches are up, and that l1 and l2 are both dark. This is represented by the atomic clauses


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


Thus, it follows that


which means that at least one of the components cb1, s1, s2, or l1 must not be ok, and at least one of the components cb1, s3, or l2 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


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:


Thus, either cb1 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_cb1}, {ok_s1,ok_s3}, {ok_s1,ok_l2}, {ok_s2,ok_s3}, {ok_s2,ok_l2}, {ok_l1,ok_s3}, {ok_l1,ok_l2}. 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 a,A, 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 {a,{a}:a is assumable}. Clauses can be used to derive new conclusions. If there is a clause hb1bm such that for each bi there is some Ai such that bi,AiC, then h,A1Am can be added to C. This covers the case of atomic clauses, with m=0, where h,{} is added to C.

1: procedure Prove_conflict_BU(KB,Assumables)
2:      Inputs
3:          KB: a set of Horn clauses
4:          Assumables: a set of atoms that can be assumed      
5:      Output
6:          set of conflicts
7:      Local
8:          C is a set of pairs of an atom and a set of assumables      
9:      C:={a,{a}:a is assumable}
10:      repeat
11:          select clause “hb1bm” in KB such that
12:          bi,AiC for all i and
13:          h,AC where A=A1Am
14:          C:=C{h,A}
15:      until no more selections are possible
16:      return {A:false,AC}
Figure 5.9: Bottom-up proof procedure for computing conflicts

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 false,A is generated, the assumptions A form a conflict.

One refinement of this program is to prune supersets of assumptions. If a,A1 and a,A2 are in C, where A1A2, then a,A2 can be removed from C or not added to C. There is no reason to use the extra assumptions to imply a. Similarly, if false,A1 and a,A2 are in C, where A1A2, then a,A2 can be removed from C because A1 and any superset – including A2 – 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


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


Thus, the knowledge base entails


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.

1: non-deterministic procedure Prove_conflict_TD(KB,Assumables)
2:      Inputs
3:          KB: a set Horn clauses
4:          Assumables: a set of atoms that can be assumed      
5:      Output
6:          A conflict
7:      Local
8:          G is a set of atoms (that implies false)      
9:      G:={false}
10:      repeat
11:          select an atom a in G such that aAssumables
12:          choose clause “aB” in KB with a as head
13:          G:=(G{a})B
14:      until  GAssumables
15:      return G
Figure 5.10: Top-down Horn clause proof procedure to find conflicts

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:


The set {ok_cb1,ok_s1,ok_s2,ok_l1} is returned as a conflict. Different choices of the clause to use can lead to another answer.