Expanding the Base Language

(14th-July-2020)

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

• On the Depth-Bounded Search, It showed how adding extra meta-level clauses can be used to expand the base language. This section shows how adding extra conditions to the meta-level clauses can reduce what can be proved.

• A useful meta-interpreter is one that implements depth-bounded search. This can be used to look for short proofs or as part of an iterative-deepening searcher, which carries out repeated depth-bounded, depth-first searches, increasing the bound at each stage.

• % bprove(G,D) is true if G can be proved with a proof tree of depth less than or equal to number D.

• bprove(true,D).

• bprove((A&B),D)←

• bprove(A,D)∧

• bprove(B,D).

• bprove(H,D)←

• D ≥ 0∧

• D1 is D-1∧

• (H⇐B)∧

• bprove(B,D1).

• Figure 13.12: A meta-interpreter for depth-bounded search