6.2 Whynot? Questions

Just as how questions let you explore the proof tree for a particular derivation, whynot questions let you explore the search tree. This facility is mainly used for determining why there was no proof for a particular query. As such the documentation is written assuming that you are trying to determine why a query failed, when you thought that it should have succeeded.

If a query fails when it should have succeeded, either there was a rule defining the query whose body fails when it should have succeeded, or else there is a missing rule for that query.

You can ask a query to determine why some query failed using: 

ailog: whynot query.

where query is a body.

If the query is an atom, you can examine each rule whose head unifies with the query. For each such rule, the system asks whether you want to trace this rule. You can reply with:

yes.
to determine why this rule failed. You should give this answer when this rule should have succeeded for this query.
no.
to ask for another rule. You give this answer if this rule should have failed for this query.
up.
to return to a previous choice point (the rule in which the atom appears, or else the top-level if the atom was the initial query).
ok.
to return to the top-level.
help.
to get a menu of available answers.

If you answer "no" to each rule, this means that all of the rules in the knowledge base should have failed, and so the appropriate rule for the query that should have succeeded is missing.

To determine why a rule failed, we determine why the body failed. If the body is atomic, we use the above whynot mechanism to determine why the rule failed. If the body of the rule is a conjunction, alpha&beta, there are four cases:

  • alpha fails, in which case we should use recursively use the whynot mechanism to determine why it failed.
  • an instance of alpha succeeds, but should not have succeeded. In this case we can use the how mechanism to debug this proof. This case arises because beta may have rightfully failed on the instance of alpha that succeeded.
  • an instance of alpha succeeds, but this instance should have lead to failure of the conjunction. In this case we should look for another proof for alpha.
  • an instance of alpha succeeds that should lead to the success of the conjunction, in which case we need to determine why beta failed on this instance.

Thus, when there is a conjunctive body, we first try to prove the leftmost conjunct. If it fails, we use the above whynot mechanism to determine why it failed. If it succeeds, the user is asked Should this answer lead to a successful proof? The user can reply:

yes.
this instance should have made the body succeed. Thus you need to debug the rest of the conjunction.
no.
this instance should lead to a failure of the body. Thus you need to try another proof for this atom.
debug.
this instance is false, debug it. This enters the how interaction.
ok.
to return to the top-level.
help.
to get a menu of available answers.
Example. Suppose we had the knowledge base from Example 4. Suppose that, the user knew that Joe had a child called Jane, and wanted to know why the system didn't think that Randy was Jane's grandfather. We could imagine the following dialogue: 
ailog: whynot grandfather(randy,jane). 
  grandfather(randy,jane) <- father(randy,A)&parent(A,jane).
    Trace this rule? [yes,no,up,help]: yes.
  The proof for father(randy,sally) succeeded.
   Should this answer lead to a successful proof? 
               [yes,no,debug,help]: no.
  The proof for father(randy,joe) succeeded.
   Should this answer lead to a successful proof? 
               [yes,no,debug,help]: yes.
  parent(joe,jane) <- mother(joe,jane).
    Trace this rule? [yes,no,up,help]: no.
  parent(joe,jane) <- father(joe,jane).
    Trace this rule? [yes,no,up,help]: yes.
  There is no applicable rule for father(joe,jane).
  parent(joe,jane) <- father(joe,jane).
    Trace this rule? [yes,no,up,help]: up.
  grandfather(randy,jane) <- father(randy,joe)&parent(joe,jane).
    Trace this rule? [yes,no,up,help]: up.
ailog: