Artificial
Intelligence

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

A number of reasons exist for providing a facility for collecting goals that should be delayed:

• to implement consistency-based diagnosis and 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. This is called partial evaluation and is used for explanation-based learning to leave out intermediate steps in a proof.

% dprove(G,D₀,D₁) is true if D₀ is an ending of D₁ and G logically follows from the conjunction of the delayable atoms in D₁.

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

Suppose you can prove dprove(G,[],D). Let D' be the conjunction of base-level atoms in the list of delayed goals D. Then you know that the implication G ←D' is a logical consequence of the clauses, and delay(d) is true for all d∈D.