14.4 Implementing Knowledge-Based Systems

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.

% 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 14.14: A meta-interpreter that collects delayed goals

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 GD is a logical consequence of the clauses, and delay(d) is true for all dD. 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


The query

𝘢𝘴𝘬 dprove(live(p1),[],D).

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

The query

𝘢𝘴𝘬 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 9.