### 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.

**Example 13.24:**An example of the kind of base-level rule you can now interpret is

*can_see ⇐eyes_open &(lit(l*

_{1})∨ lit(l_{2})),which says that *can_see* is *true* if
*eyes_open* is *true* and either
*lit(l _{1})* or

*lit(l*is

_{2})*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(true).*

*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(call(G))←*

*prove(G).*