14.4.2 A Vanilla Meta-Interpreter

This section presents a very simple vanilla meta-interpreter for the definite clause language written in the definite clause language. Subsequent sections augment this meta-interpreter to provide extra language constructs and knowledge engineering tools. It is important to first understand the simple case before considering the more sophisticated meta-interpreters presented later.

% $prove(G)$ is true if base-level body $G$ is a logical consequence of the base-level clauses that are defined using the predicate symbol “ $\Leftarrow\mbox{}$ ”.

	$\displaystyle{prove(true).}$
	$\displaystyle{prove((A\>\&\>B))\leftarrow\mbox{}}$
	$\displaystyle\ \ \ \ {prove(A)\wedge\mbox{}}$
	$\displaystyle\ \ \ \ {prove(B).}$
	$\displaystyle{prove(H)\leftarrow\mbox{}}$
	$\displaystyle\ \ \ \ {(H\Leftarrow\mbox{}B)\wedge\mbox{}}$
	$\displaystyle\ \ \ \ {prove(B).}$

Figure 14.9: The vanilla definite clause meta-interpreter

Figure 14.9 defines a meta-interpreter for the definite clause language. This is an axiomatization of the relation $p r o v e$ , where $prove(G)$ is true when base-level body $G$ is a logical consequence of the base-level clauses.

As with axiomatizing any other relation, we write the clauses that are true in the intended interpretation, ensuring that they cover all of the cases and that there is some simplification through recursion. This meta-interpreter essentially covers each of the cases allowed in the body of a clause or in a query, and it specifies how to solve each case. A body is either empty, a conjunction, or an atom. The empty base-level body $t r u e$ is trivially proved. To prove the base-level conjunction $A\>\&\>B$ , prove $A$ and prove $B$ . To prove atom $H$ , find a base-level clause with $H$ as the head, and prove the body of the clause.

	$\displaystyle{lit(L)\Leftarrow\mbox{}}$
	$\displaystyle\ \ \ \ {light(L)\>\&\>}$
	$\displaystyle\ \ \ \ {ok(L)\>\&\>}$
	$\displaystyle\ \ \ \ {live(L).}$
	$\displaystyle{live(W)\Leftarrow\mbox{}}$
	$\displaystyle\ \ \ \ {connected\_to(W,W_{1})\>\&\>}$
	$\displaystyle\ \ \ \ {live(W_{1}).}$
	$\displaystyle{live(outside)\Leftarrow\mbox{}true.}$
	$\displaystyle{light(l_{1})\Leftarrow\mbox{}true.}$
	$\displaystyle{light(l_{2})\Leftarrow\mbox{}true.}$
	$\displaystyle{down(s_{1})\Leftarrow\mbox{}true.}$
	$\displaystyle{up(s_{2})\Leftarrow\mbox{}true.}$
	$\displaystyle{up(s_{3})\Leftarrow\mbox{}true.}$
	$\displaystyle{connected\_to(l_{1},w_{0})\Leftarrow\mbox{}true.}$
	$\displaystyle{connected\_to(w_{0},w_{1})\Leftarrow\mbox{}up(s_{2})\>\&\>ok(s_{% 2}).}$
	$\displaystyle{connected\_to(w_{0},w_{2})\Leftarrow\mbox{}down(s_{2})\>\&\>ok(s% _{2}).}$
	$\displaystyle{connected\_to(w_{1},w_{3})\Leftarrow\mbox{}up(s_{1})\>\&\>ok(s_{% 1}).}$
	$\displaystyle{connected\_to(w_{2},w_{3})\Leftarrow\mbox{}down(s_{1})\>\&\>ok(s% _{1}).}$
	$\displaystyle{connected\_to(l_{2},w_{4})\Leftarrow\mbox{}true.}$
	$\displaystyle{connected\_to(w_{4},w_{3})\Leftarrow\mbox{}up(s_{3})\>\&\>ok(s_{% 3}).}$
	$\displaystyle{connected\_to(p_{1},w_{3})\Leftarrow\mbox{}true.}$
	$\displaystyle{connected\_to(w_{3},w_{5})\Leftarrow\mbox{}ok(cb_{1}).}$
	$\displaystyle{connected\_to(p_{2},w_{6})\Leftarrow\mbox{}true.}$
	$\displaystyle{connected\_to(w_{6},w_{5})\Leftarrow\mbox{}ok(cb_{2}).}$
	$\displaystyle{connected\_to(w_{5},outside)\Leftarrow\mbox{}true.}$
	$\displaystyle{ok(X)\Leftarrow\mbox{}true.}$

Figure 14.10: A knowledge base for house wiring

Example 14.19.

Consider Figure 14.10 adapted from Example 13.12. This can be seen from meta-level as a knowledge base of atoms, all with the same predicate symbol $\Leftarrow\mbox{}$ . It can also be viewed as base-level knowledge base consisting of multiple rules. The vanilla meta-interpreter sees it as a collection of atoms.

The base-level goal $live(w_{5})$ is asked with the following query to the meta-interpreter:

\displaystyle{\mbox{{ask}~{}}~{}prove(live(w_{5})).}

The third clause of $p r o v e$ is the only clause matching this query. It then looks for a clause of the form $live(w_{5})\Leftarrow\mbox{}B$ and finds

\displaystyle{live(W)\Leftarrow\mbox{}connected\_to(W,W_{1})\>\&\>live(W_{1}).}

$W$ unifies with $w_{5}$ , and $B$ unifies with $connected\_to(w_{5},W_{1})\>\&\>live(W_{1})$ . It then tries to prove

\displaystyle{prove((connected\_to(w_{5},W_{1})\>\&\>live(W_{1}))).}

The second clause for $p r o v e$ is applicable. It then tries to prove

\displaystyle{prove(connected\_to(w_{5},W_{1})).}

Using the third clause for $p r o v e$ , it looks for a clause with a head to unify with

connected\_to(w_{5},W_{1})\Leftarrow\mbox{}B,

and find $connected\_to(w_{5},outside)\Leftarrow\mbox{}true$ , binding $W_{1}$ to $o u t s i d e$ . It then tries to prove $prove(true)$ , which succeeds using the first clause for $p r o v e$ .

The second half of the conjunction, $prove(live(W_{1}))$ with $W_{1}=outside$ , reduces to $prove(true)$ which is, again, immediately solved.

Artificial Intelligence 2E

14.4.2 A Vanilla Meta-Interpreter

Example 14.19.

Artificial
Intelligence 2E