Third edition of Artificial Intelligence: foundations of computational agents, Cambridge University Press, 2023 is now available (including the full text).
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((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 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, "D1 is D-1" is true if D1 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 13.7.)
