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,D0,D1) is true if D0 is an ending of D1 and G logically follows from the conjunction of the delayable atoms in D1.

Figure 13.16: A meta-interpreter that collects delayed goals

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.

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

The query

ask dprove(live(p1),[],D).

has one answer, namely, D=[ok(cb1)]. If ok(cb1) were true, then live(p1) would be true. The query

ask dprove((lit(l2)&live(p1)),[],D).

has the answer D=[ok(cb1),ok(cb1),ok(s3)]. If cb1 and s3 are ok, then l2 will be lit and p1 will be live.

Note that ok(cb1) 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 13.8.