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((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).
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.3.3.1 traverse this tree. The user only has to see clauses, not this tree. See Exercise 13.12.