#### 5.3.4.2 Missing Answers

The second type of error occurs when an expected answer is not
produced. This manifests itself by a failure when an answer is
expected. A goal *g* that is true in the domain, but is not a
consequence of the knowledge base, is called a **false-negative
error**.

The preceding algorithm does not work in this case. There is no
proof. We must look for why there is no proof for *g*.

An appropriate answer is not produced only if a definite clause or clauses are missing from the knowledge base. By knowing the intended interpretation of the symbols and by knowing what queries should succeed (i.e, what is true in the intended interpretation), a domain expert can debug a missing answer. Given an atom that failed when it should have succeeded, Figure 5.7 shows how to find an atom for which there is a missing definite clause.

**Procedure**DebugMissing(

*g,KB*)

2:

**Inputs**

3:

*KB*a knowledge base

4:

*g*an atom:

*KB⊬ g*and

*g*is

*true*in the intended interpretation

5:

**Output**

6: atom for which there is a clause missing

7:

**if**(there is a definite clause

*g←a*such that all

_{1}∧...∧a_{k}∈KB*a*are true in the intended interpretation)

_{i}**then**

8:

**select**

*a*that cannot be proved

_{i}9:

*DebugMissing(a*

_{i},KB)10:

**else**

11:

**return**

*g*

Suppose
*g* is an atom that
should have a proof, but which fails. Because the proof for *g* fails, the bodies of all of the
definite clauses with *g* in the head fail.

- Suppose one of these definite clauses for
*g*should have resulted in a proof; this means all of the atoms in the body must be true in the intended interpretation. Because the body failed, there must be an atom in the body that fails. This atom is then true in the intended interpretation, but fails. So we can recursively debug it. - Otherwise, there
is no definite clause applicable to proving
*g*, so the user must add a definite clause for*g*.

**Example 5.15:**Suppose that, for the axiomatization of the electrical domain in Example 5.5, the world of Figure 1.8 actually had

*s*down. Thus, it is missing the definite clause specifying that

_{2}*s*is down. The axiomatization of Example 5.5 fails to prove

_{2}*lit_l*when it should succeed. Let's find the bug.

_{1}*lit_l _{1}* failed, so we find all of the rules with

*lit_l*in the head. There is one such rule:

_{1}*lit_l*

_{1}←light_l_{1}∧live_l_{1}∧ok_l_{1}.The user can then verify that all of the elements of the body are true.
*light_l _{1}* and

*ok_l*can both be derived, but

_{1}*live_l*fails, so we debug this atom. There is one rule with

_{1}*live_l*in the head:

_{1}*live_l*

_{1}←live_w_{0}.The atom *live_w _{0}* cannot be proved, but
the user verifies that it is true in the intended interpretation. So we
find the rules for

*live_w*:

_{0}*live_w*

live_w_0 ←live_w_2 ∧down_s_2.

_{0}←live_w_{1}∧up_s_{2}.The user can say that the body of the second rule is true. A
proof exists for *live_w _{2}*, but there
are no definite clauses for

*down_s*, so this atom is returned. The correction is to add the appropriate atomic clause or rule for it.

_{2}