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

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.

1: 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←a1∧...∧ak∈KB such that all ai are true in the intended interpretation) then
8:           select ai that cannot be proved
9:                     DebugMissing(ai,KB)
10:           else
11:                     return g
Figure 5.7: An algorithm for debugging missing answers

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 s2 down. Thus, it is missing the definite clause specifying that s2 is down. The axiomatization of Example 5.5 fails to prove lit_l1 when it should succeed. Let's find the bug.

lit_l1 failed, so we find all of the rules with lit_l1 in the head. There is one such rule:

lit_l1 ←light_l1 ∧live_l1 ∧ok_l1.

The user can then verify that all of the elements of the body are true. light_l1 and ok_l1 can both be derived, but live_l1 fails, so we debug this atom. There is one rule with live_l1 in the head:

live_l1 ←live_w0.

The atom live_w0 cannot be proved, but the user verifies that it is true in the intended interpretation. So we find the rules for live_w0:

live_w0 ←live_w1 ∧up_s2.
live_w_0 ←live_w_2 ∧down_s_2.

The user can say that the body of the second rule is true. A proof exists for live_w2, but there are no definite clauses for down_s2, so this atom is returned. The correction is to add the appropriate atomic clause or rule for it.