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

13.5.5 Meta-interpreter to Build Proof Trees

To implement the how command of Section 5.3.3.1, the interpreter maintains a representation of the proof tree for a derived answer. Our meta-interpreter can be extended to build a proof tree. Figure 13.13 gives a meta-interpreter that implements built-in predicates and builds a representation of a proof tree. This proof tree can be traversed to implement how questions.

% hprove(G,T) is true if base-level body G is a logical consequence of the base-level knowledge base, and T is a representation of the proof tree for the corresponding proof.

hprove(true,true).
hprove((A&B),(L&R))←
     hprove(A,L)∧
     hprove(B,R).
hprove(H,if(H,built_in))←
     built_in(H)∧
     call(H).
hprove(H,if(H,T))←
     (H⇐B)∧
     hprove(B,T).
Figure 13.13: A meta-interpreter that builds a proof tree
Example 13.25: Consider the base-level clauses for the wiring domain and the base-level query ask lit(L). There is one answer, namely L=l2. The meta-level query ask hprove(lit(L),T) returns the answer L=l2 and the tree
                                                               
T=if(lit(l2),
if(light(l2),true)&
if(ok(l2),true)&
if(live(l2),
if(connected_to(l2,w4),true)&
if(live(w4),
if(connected_to(w4,w3),
if(up(s3),true))&
if(live(w3),
if(connected_to(w3,w5),
if(ok(cb1),true))&
if(live(w5),
if(connected_to(w5,outside),true)&
if(live(outside),true)))))).

Although this tree can be understood if properly formatted, it requires a skilled user to understand it. The how questions of Section 5.3.3.1 traverse this tree. The user only has to see clauses, not this tree. See Exercise 13.12.