Artificial
Intelligence

13.5.6 Ask the User Meta-interpreter

% aprove(G) is true if base-level body G is a logical consequence of the base-level knowledge base and the answers provided by asking the user yes/no questions.

Figure 13.14 gives a pseudocode interpreter that incorporates querying the user. This interpreter assumes that there is some extralogical external database recording answers to queries. The database is updated as queries are answered. Meta-level facts of the form answered(H,Ans) are being added. ask(H,Ans) is true if H is asked of the user; and Ans, either yes or no, is given by the user as a reply. unanswered(H) means answered(H,Ans) is not in the database for any Ans. Note that the intended meaning of the fourth clause is that it succeeds only if the answer is yes, but the answer gets recorded whether the user answered yes or no.

% wprove(G,A) is true if base-level body G is a logical consequence of the base-level knowledge base, and A is a list of ancestors for G in the proof tree for the original query.

Figure 13.15 gives a meta-interpreter that can be used to find the list of ancestor rules for a why question. The second argument to wprove is a list of clauses of the form (H⇐B) for each head of a rule in the current part of the proof tree. This meta-interpreter can be combined with the meta-interpreter of Figure 13.14 that actually asks questions. When the user is asked a question and responds with "why," the list can be used to give the set of rules used to generate the current subgoal. The "why" described in Section 5.3.3.2 can be implemented by stepping through the list and, thus, up the proof tree, one step at a time.