### 13.5.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
"*⇐*".

*prove(true).*

*prove((A&B))←*

*prove(A)∧*

*prove(B).*

*prove(H)←*

*(H⇐B)∧*

*prove(B).*

Figure 13.9 defines a meta-interpreter for the
definite clause language. This is an axiomatization of the relation
*prove*; *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 *true* 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.

*lit(L) ⇐*

*light(L)&*

*ok(L)&*

*live(L).*

*live(W) ⇐*

*connected_to(W,W*

_{1})&*live(W*

_{1}).*live(outside)⇐true.*

*light(l*

_{1})⇐true.*light(l*

_{2})⇐true.*down(s*

_{1})⇐true.*up(s*

_{2})⇐true.*up(s*

_{3})⇐true.*connected_to(l*

_{1},w_{0})⇐true.*connected_to(w*

connected_to(w_0,w_2) ⇐down(s_2)&ok(s_2).

_{0},w_{1}) ⇐up(s_{2})&ok(s_{2}).*connected_to(w*

connected_to(w_2,w_3) ⇐down(s_1)&ok(s_1).

_{1},w_{3}) ⇐up(s_{1})&ok(s_{1}).*connected_to(l*

_{2},w_{4})⇐true.*connected_to(w*

connected_to(p_1,w_3)⇐true.

_{4},w_{3}) ⇐up(s_{3})&ok(s_{3}).*connected_to(w_3,w_5) ⇐ok(cb_1).*

*connected_to(p*

_{2},w_{6})⇐true.*connected_to(w*

connected_to(w_5,outside)⇐true.

_{6},w_{5}) ⇐ok(cb_{2}).*ok(X)⇐true.*

*
*

*⇐*

**Example 13.23:**Consider the meta-level representation of the base-level knowledge base in Figure 13.10. This knowledge base is adapted from Example 12.11. This knowledge base consists of meta-level atoms, all with the same predicate symbol, namely "*". Here, we describe how a top-down implementation works given the knowledge base that consists of the vanilla meta-interpreter and the clauses for "*⇐

*".*

*The base-level goal *live(w_5)* is asked with the following query:
*

**ask**prove(live(w_5)).

*The third clause of *prove* is the only clause matching this
query. It then looks for a clause of the form *live(w_5) ⇐B* and
finds
*

*live(W) ⇐connected_to(W,W_1)&live(W_1).*

*W* unifies with *w _{5}*, and

*B*unifies with

*connected_to(w*. It then tries to prove

_{5},W_{1})&live(W_{1})*prove((connected_to(w*

_{5},W_{1})&live(W_{1}))).The second clause for *prove* is applicable. It then tries to prove

*prove(connected_to(w*

_{5},W_{1})).Using the third clause for *prove*, it looks for a clause with a head to unify with

connected_to(w_{5},W_{1})⇐B,

and find *connected_to(w _{5},outside)⇐true*, binding

*W*to

_{1}*outside*. It then tries to prove

*prove(true)*, which succeeds using the first clause for

*prove*.

The second half of the conjunction,
*prove(live(W _{1}))* with

*W*, reduces to

_{1}=outside*prove(true)*which is, again, immediately solved.