5.3.4.1 Incorrect Answers

An incorrect answer is an answer that has been proved yet is false in the intended interpretation. It is also called a false-positive error. An incorrect answer can only be produced by a sound proof procedure if an incorrect definite clause was used in the proof.

Assume that whoever is debugging the knowledge base, such as a domain expert or a user, knows the intended interpretation of the symbols of the language and can determine whether a particular proposition is true or false in the intended interpretation. The person does not have to know how the answer was derived. To debug an incorrect answer, a domain expert needs only to answer yes-or-no questions.

Suppose there is an atom g that was proved yet is false in the intended interpretation. Then there must be a rule g←a1∧...∧ak in the knowledge base that was used to prove g. Either

  • one of the ai is false in the intended interpretation, in which case it can be debugged in the same way, or
  • all of the ai are true in the intended interpretation. In this case, the definite clause g←a1∧...∧ak must be incorrect.

This leads to an algorithm, presented in Figure 5.6, to debug a knowledge base when an atom that is false in the intended interpretation is derived.

1: Procedure Debug(g,KB)
2:           Inputs
3:                     KB a knowledge base
4:                     g an atom: KB |- g and g is false in intended interpretation
5:           Output
6:                     clause in KB that is false
7:           Find definite clause g←a1∧...∧ak∈KB used to prove g
8:           for each ai do
9:                     ask user whether ai is true
10:                     if (user specifies ai is false) then
11:                               return Debug(ai,KB)
12:                     
13:           
14:           return g←a1∧...∧ak
Figure 5.6: An algorithm to debug incorrect answers

This only requires the person debugging the knowledge base to be able to answer yes-or-no questions.

This procedure can also be carried out by the use of the how command. Given a proof for g that is false in the intended interpretation, a user can ask how that atom was proved. This will return the definite clause that was used in the proof. If the clause was a rule, the user could use how to ask about an atom in the body that was false in the intended interpretation. This will return the rule that was used to prove that atom. The user can repeat this until a definite clause is found where all of the elements of the body are true (or there are no elements in the body). This is the incorrect definite clause. The method of debugging assumes that the user can determine whether an atom is true or false in the intended interpretation. The user does not have to know the proof procedure used.

Example 5.14: Consider Example 5.5, involving the electrical domain, but assume there is a bug in the program. Suppose that the domain expert or user had inadvertently said that whether w1 is connected to w3 depends on the status of s3 instead of s1 (see Figure 1.8). Thus, the knowledge includes the following incorrect rule:
live_w1 ←live_w3 ∧up_s3.

All of the other axioms are the same as in Example 5.5. Given this axiom set, the atom lit_l1 can be derived, which is false in the intended interpretation. Consider how a user would go about finding this incorrect definite clause when they detected this incorrect answer.

Given that lit_l1 is false in the intended interpretation, they ask how it was derived, which will give the following rule:

lit_l1 ←light_l1 ∧live_l1 ∧ok_l1.

They check the atoms in the body of this rule. light_l1 and ok_l1 are true in the intended interpretation, but live_l1 is false in the intended interpretation. So they ask

how 2.

The system presents the rule

live_l1 ←live_w0.

live_w0 is false in the intended interpretation, so they ask

how 1.

The system presents the rule

live_w0 ←live_w1 ∧up_s2.

live_w_1 is false in the intended interpretation, so they ask

how 1.

The system presents the rule

live_w_1 ←live_w_3 ∧up_s_3.

Both elements of the body are true in the intended interpretation, so this is the buggy rule.

The user or domain expert can find the buggy definite clause without having to know the internal workings of the system or how the proof was found. They only require knowledge about the intended interpretation and the disciplined use of how.