# 14.4.6 Delaying Goals

One of the most useful abilities of a meta-interpreter is to delay goals. Some goals, rather than being proved, can be collected in a list. At the end of the proof, the system derives the implication that, if the delayed goals were all true, the computed answer would be true.

Providing a facility for collecting goals that should be delayed is useful for a number of reasons:

• to implement proof by contradiction as used in consistency-based diagnosis or to implement abduction, the assumables are delayed

• to delay subgoals with variables, in the hope that subsequent calls will ground the variables, and

• to create new rules that leave out intermediate steps – for example, if the delayed goals are to be asked of a user or queried from a database.

Figure 14.14 gives a meta-interpreter that provides delaying. A base-level atom $G$ can be made delayable using the meta-level fact $delay(G)$. The delayable atoms can be collected into a list without being proved.

If you can prove $dprove(G,[\,],D)$, you know that the implication $G\Leftarrow\mbox{}D$ is a logical consequence of the clauses, and $delay(d)$ is true for all $d\in D$. This idea of deriving a new clause from a knowledge base is an instance of partial evaluation. It is the basis for explanation-based learning which treats the derived clauses as learned clauses that can replace the original clauses.

###### Example 14.22.

As an example of delaying for consistency-based diagnosis, consider the base-level knowledge base of Figure 14.10, but without the rules for $ok$. Suppose, instead, that $ok(G)$ is delayable. This is represented as the meta-level fact

 $delay(ok(G)).$

The query

 $\mbox{{ask}~{}}~{}dprove(live(p_{1}),[\,],D).$

has one answer, namely, $D=[ok(cb_{1})]$. If $ok(cb_{1})$ were true, then $live(p_{1})$ would be true.

The query

 $\mbox{{ask}~{}}~{}dprove((lit(l_{2})\>\&\>live(p_{1})),[\,],D).$

has the answer $D=[ok(cb_{1}),ok(cb_{1}),ok(s_{3})]$. If $cb_{1}$ and $s_{3}$ are $ok$, then $l_{2}$ will be lit and $p_{1}$ will be live.

Note that $ok(cb_{1})$ appears as an element of this list twice. $dprove$ does not check for multiple instances of delayables in the list. A less naive version of $dprove$ would not add duplicate delayables. See Exercise 9.