### 13.5.4 Depth-Bounded Search

The previous section 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∧*

*D*

_{1}is D-1∧*(H⇐B)∧*

*bprove(B,D*

_{1}).Figure 13.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 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} is D-1*" is true
if

*D*is one less than the number

_{1}*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 13.7.)