14.4 Implementing Knowledge-Based Systems

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.

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

Figure 14.13: A meta-interpreter that builds a proof tree
Example 14.21.

Consider the base-level clauses for the wiring domain and the base-level query 𝖺𝗌𝗄 lit(L). There is one answer, namely L=l2. The meta-level query 𝖺𝗌𝗄 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.4.3 traverse this tree. The user only has to see clauses, not this tree. See Exercise 13.