# 14.4.5 Meta-Interpreter to Build Proof Trees

To implement the how question of Section 5.4.3, the interpreter can build a proof tree for a derived answer. Figure 14.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. In this algorithm, a proof tree is either $true$, $built\_in$, of the form $if(G,T)$ where $G$ is an atom and $T$ is a proof tree, or of the form $(L\>\&\>R)$ where $L$ and $R$ are proof trees.

###### Example 14.21.

Consider the base-level clauses for the wiring domain and the base-level query $\mbox{{ask}~{}}~{}lit(L)$. There is one answer, namely $L=l_{2}$. The meta-level query $\mbox{{ask}~{}}~{}hprove(lit(L),T)$ returns the answer $L=l_{2}$ and the tree $T=if(lit(l_{2}),$ $if(light(l_{2}),true)\>\&\>$ $if(ok(l_{2}),true)\>\&\>$ $if(live(l_{2}),$ $if(connected\_to(l_{2},w_{4}),true)\>\&\>$ $if(live(w_{4}),$ $if(connected\_to(w_{4},w_{3}),$ $if(up(s_{3}),true))\>\&\>$ $if(live(w_{3}),$ $if(connected\_to(w_{3},w_{5}),$ $if(ok(cb_{1}),true))\>\&\>$ $if(live(w_{5}),$ $if(connected\_to(w_{5},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.4.3 traverse this tree. The user only has to see clauses, not this tree. See Exercise 13.