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