5.5 Proving by Contradiction

The third edition of Artificial Intelligence: foundations of computational agents, Cambridge University Press, 2023 is now available (including full text).

5.5.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.23.

Consider the house wiring example depicted in Figure 5.2 and represented in Example 5.7. A background knowledge base suitable for consistency-based diagnosis is given in Figure 5.8. 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:

𝑓𝑎𝑙𝑠𝑒dark_l1lit_l1.
𝑓𝑎𝑙𝑠𝑒dark_l2lit_l2.
light_l1.
light_l2.
live_outside.
live_l1live_w0.
live_w0live_w1up_s2ok_s2.
live_w0live_w2down_s2ok_s2.
live_w1live_w3up_s1ok_s1.
live_w2live_w3down_s1ok_s1.
live_l2live_w4.
live_w4live_w3up_s3ok_s3.
live_p1live_w3.
live_w3live_w5ok_cb1.
live_p2live_w6.
live_w6live_w5ok_cb2.
live_w5live_outside.
lit_l1light_l1live_l1ok_l1.
lit_l2light_l2live_l2ok_l2.
𝑓𝑎𝑙𝑠𝑒dark_l1lit_l1.
𝑓𝑎𝑙𝑠𝑒dark_l2lit_l2.
𝘢𝘴𝘴𝘶𝘮𝘢𝘣𝘭𝘦ok_cb1,ok_cb2,ok_s1,ok_s2,ok_s3,ok_l1,ok_l2.
Figure 5.8: Knowledge for Example 5.23

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

up_s1.
up_s2.
up_s3.
dark_l1.
dark_l2.

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

{ok_cb1,ok_s1,ok_s2,ok_l1}
{ok_cb1,ok_s3,ok_l2}.

Thus, it follows that

𝐾𝐵¬ok_cb1¬ok_s1¬ok_s2¬ok_l1
𝐾𝐵¬ok_cb1¬ok_s3¬ok_l2,

which means that at least one of the components cb1, s1, s2, or l1 must not be ok, and 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, given a set of conflicts, it is often difficult to determine whether all of the conflicts could be explained by a few faults. Some of the questions that a user may want to know are whether all of the conflicts could be accounted for a by a single fault or a pair of 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.24.

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

(¬ok_cb1¬ok_s1¬ok_s2¬ok_l1)
    (¬ok_cb1¬ok_s3¬ok_l2)

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:

¬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).

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.