Third edition of Artificial Intelligence: foundations of computational agents, Cambridge University Press, 2023 is now available (including the full text).

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: The vanilla definite clause meta-interpreter

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,W1)&
     live(W1).
live(outside)⇐true.
light(l1)⇐true.
light(l2)⇐true.
down(s1)⇐true.
up(s2)⇐true.
up(s3)⇐true.
connected_to(l1,w0)⇐true.
connected_to(w0,w1) ⇐up(s2)&ok(s2).
connected_to(w_0,w_2) ⇐down(s_2)&ok(s_2).
connected_to(w1,w3) ⇐up(s1)&ok(s1).
connected_to(w_2,w_3) ⇐down(s_1)&ok(s_1).
connected_to(l2,w4)⇐true.
connected_to(w4,w3) ⇐up(s3)&ok(s3).
connected_to(p_1,w_3)⇐true.
connected_to(w_3,w_5) ⇐ok(cb_1).
connected_to(p2,w6)⇐true.
connected_to(w6,w5) ⇐ok(cb2).
connected_to(w_5,outside)⇐true.
ok(X)⇐true.
Figure 13.10: A base-level knowledge base for house wiring
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 w5, and B unifies with connected_to(w5,W1)&live(W1). It then tries to prove

prove((connected_to(w5,W1)&live(W1))).

The second clause for prove is applicable. It then tries to prove

prove(connected_to(w5,W1)).

Using the third clause for prove, it looks for a clause with a head to unify with

connected_to(w5,W1)⇐B,

and find connected_to(w5,outside)⇐true, binding W1 to outside. It then tries to prove prove(true), which succeeds using the first clause for prove.

The second half of the conjunction, prove(live(W1)) with W1=outside, reduces to prove(true) which is, again, immediately solved.