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 $t r u e$ , $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.

	$\displaystyle{hprove(true,true).}$
	$\displaystyle{hprove((A\>\&\>B),(L\>\&\>R))\leftarrow\mbox{}}$
	$\displaystyle\ \ \ \ {hprove(A,L)\wedge\mbox{}}$
	$\displaystyle\ \ \ \ {hprove(B,R)}.$
	$\displaystyle{hprove(H,if(H,built\_in))\leftarrow\mbox{}}$
	$\displaystyle\ \ \ \ {built\_in(H)\wedge\mbox{}}$
	$\displaystyle\ \ \ \ {call(H).}$
	$\displaystyle{hprove(H,if(H,T))\leftarrow\mbox{}}$
	$\displaystyle\ \ \ \ {(H\Leftarrow\mbox{}B)\wedge\mbox{}}$
	$\displaystyle\ \ \ \ {hprove(B,T).}$

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 $\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.

Artificial Intelligence 2E

14.4.5 Meta-Interpreter to Build Proof Trees

Example 14.21.

Artificial
Intelligence 2E