### 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.