Third edition of Artificial Intelligence: foundations of computational agents, Cambridge University Press, 2023 is now available (including the full text).
13.5.3 Expanding the Base Language
The base language can be changed by modifying the meta-interpreter. Adding clauses is used to increase what can be proved. Adding extra conditions to the meta-interpreter rules can restrict what can be proved.
In all practical systems, not every predicate is defined by clauses. For example, it would be impractical to axiomatize arithmetic on current machines that can do arithmetic quickly. Instead of axiomatizing such predicates, it is better to call the underlying system directly. Assume the predicate call(G) evaluates G directly. Writing call(p(X)) is the same as writing p(X). The predicate call is required because the definite clause language does not allow free variables as atoms.
Built-in procedures can be evaluated at the base level by defining the meta-level relation built_in(X) that is true if all instances of X are to be evaluated directly; X is a meta-level variable that must denote a base-level atom. Do not assume that "built_in" is provided as a built-in relation. It can be axiomatized like any other relation.
The base language can be expanded to allow for disjunction (inclusive or) in the body of a clause.
The disjunction, A∨ B, is true in an interpretation I when either A is true in I or B is true in I (or both are true in I).
Allowing disjunction in the body of base-level clauses does not require disjunction in the metalanguage.
which says that can_see is true if eyes_open is true and either lit(l1) or lit(l2) is true (or both).
Figure 13.11 shows a meta-interpreter that allows built-in procedures to be evaluated directly and allows disjunction in the bodies of rules. This requires a database of built-in assertions and assumes that call(G) is a way to prove G in the meta-level.
% prove(G) is true if base-level body G is a logical consequence of the base-level knowledge base.
prove((A&B))←
prove(A) ∧
prove(B).
prove((A∨ B))←
prove(A).
prove((A∨ B))←
prove(B).
prove(H)←
built_in(H) ∧
call(H).
prove(H)←
(H⇐B)∧
prove(B).
Given such an interpreter, the meta-level and the base level are different languages. The base level allows disjunction in the body. The meta-level does not require disjunction to provide it for the base language. The meta-level requires a way to interpret call(G), which the base level cannot handle. The base level, however, can be made to interpret the command call(G) by adding the following meta-level clause:
prove(G).
