The previous section showed how extra meta-level clauses can expand the base language. This section shows how adding extra conditions to meta-level clauses can restrict 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.

Figure 14.12 gives an axiomatization of the relation $bprove(G,D)$, which is true if $G$ can be proved with a proof tree of depth less than or equal to non-negative integer $D$. This figure uses Prolog’s infix predicate symbol “is”, where “$V\text{ is }E$” is true if $V$ is the numerical value of expression $E$. Within the expression, “$-$” is the infix subtraction function symbol. Thus, “$D_1\text{ is }D-1$” is true if $D_1$ is one less than the number $D$.

One aspect of this meta-interpreter is that, if $D$ is bound to a number in the query, this meta-interpreter will never go into an infinite loop. It will miss proofs whose depth is greater than $D$. As a result, this interpreter is incomplete when $D$ is set to a fixed number. However, every proof that can be found for the $prove$ meta-interpreter can be found for this meta-interpreter if the value $D$ is set large enough. The idea behind an iterative-deepening searcher is to exploit this fact by carrying out repeated depth-bounded searches, each time increasing the depth bound. Sometimes the depth-bounded meta-interpreter can find proofs that $prove$ cannot. This occurs when the $prove$ meta-interpreter goes into an infinite loop before exploring all proofs.

This is not the only way to build a bounded meta-interpreter. An alternative measure of the size of proof trees could also be used. For example, you could use the number of nodes in the tree instead of the maximum depth of the proof tree. You could also make conjunction incur a cost by changing the second rule. (See Exercise 8.)