Recycling Computed Answers in Rewrite Systems for Abduction

1 Introduction

Logic programming with answer sets [Gelfond and Lifschitz, 1988] or partial stable models [Przymusinski, 1990] has been adopted as a framework for abduction, and a number of formalisms and top-down query answering procedures have been proposed [Dung, 1991; Eshghi and Kowalski, 1989; Kakas and Mancarella, 1990; Kakas et at., 2000; Lin and You, 200 I; Satoh and I wayama, 1992].

The question we shall address in this paper is the following. With a sound and complete procedure for abduction, suppose we have computed explanations (conveniently represented as a disjunction) Es = E1 V ... V En for observation q. Suppose also that in the course of computing explanations for another observation p, we run into q again. Now, we may use the proofs Es for q without actually proving q again. The ques­ tion is this: will the use of the proofs Es for q in the proof for p preserve the soundness and completeness of the procedure?

In this paper, we answer this question positively, but in a nontrivial way, for the class of rewrite procedures proposed

*This author's work was supported in part by HK RGC CERG HKUST6205/02E.

Jia-Huai You

http:/ /www.cs. ualberta.car you Department of Computer Science University of Alberta Edmonton, Alberta, Canada

in [Lin and You, 2001]. The main result is a theorem (Theo­ rem 4.6) that says recycling preserves the soundness and com­ pleteness.

The class of rewrite procedures proposed in [Lin and You, 2001] is based on the idea of abduction as confluent and terminating rewriting. These systems are called canonical systems in the literature of rewrite systems [Dershowitz and Jouannaud, 1990]. The confluence and termination properties guarantee that rewriting terminates at a unique normal form independent of the order of rewriting. Thus, each particular strategy of rewriting yields a rewrite procedure.

The general idea of recycling is not new. Recycling in systems based on classic logic is always possible, since inferences in these systems can be viewed as transform­ ing a logic theory to a logically equivalent one. In dy­ namic programming, it is the use of the answers for pre­ viously computed subgoals that reduces the computational complexity. In some game playing programs, for ex­ ample in the world champion checker program Shinook (www.cs.ualberta.car chinook), the endgame database stores the computed results for endgame situations which can be ref­ erenced in real-time efficiently.

However, the problem of recycling in a nonmonotonic proof system has rarely been investigated. We note that recy­ cling is to use previous proofs. This differs from adding con­ sequences. For example, it is known that the semantics based on answer sets or (maximal) partial stable models do not pos­ sess the cautious nonmonotonicity property. That is, adding a consequence of a program could gain additional models thus losing some consequences. The following example is due to Dix [1991]:

P has only one answer set, {a, c}. Thus, c is a consequence. When augmented with the rule c +-,the program gains a sec­ ond answer set, {b, c}, and loses a as a consequence.

The next section defines logic program semantics. Sec­ tion 3 reviews the rewriting framework. Then in Section 4 we formulate rewrite systems with computed rules and prove that recycling preserves soundness and completeness. Sec­ tion 5 extends this result to rewrite systems with abduction, and Section 6 reports some experimental results.

2 Logic Program Semantics

A rule is of the form

where a, bi and Ci are atoms of the underlying propositional language £ . not Ci are called default negations. A literal is an atom ¢> or its negation -.¢>. A (normal) program is a fi­ nite set of rules. The completion of a program P, denoted Comp(P), is a set of equivalences: for each atom ¢> E £ , if ¢> does not appear as the head of any rule in P, ¢> +-> F E Comp(P); otherwise, ¢> +-> B1 V ... V Bn E Comp(P) (with default negations replaced by the corresponding negative lit­ erals) if there are exactly n rules ¢> +- Bi E P with ¢> as the head. We write T for Bi if Bi is empty.

The rewriting system of [Lin and You, 2001] is sound and complete w.r.t. the partial stable model semantics [Przy­ musinski, 1990]. A simple way to define partial stable models without even introducing 3-valued logic is by the so called al­ ternatingfixpoints [You and Yuan, 1995]. Let P be a program and Sa set of default negations. Define a function over sets S of default negations: Fp(S) = {not a I PUS If a} . There­ lation 1- is the standard propositional derivation relation with each default negation not ¢> being treated as a named atom not -cl>·

A partial stable model M is defined by a fixpoint of the function that applies Fp twice, F~(S) = S, while satisfying S ~ Fp(S), in the following way: for any atom ~. -,~ E M if not~ E S, ~ E M if PUS 1- ~.and~ is undefined otherwise. An answer set E is defined by a fixpoint S such that Fp(S) =SandE={~ E £I PUS 1- 0.

3 Goal Rewrite Systems

We introduce goal rewrite systems as formulated in [Lin and You, 2001].

A goal rewrite system is a rewrite system that consists of three types of rewrite rules: (1) Program rules from Comp(P) for literal rewriting; (2) Simplification rules to transform and simplify goals; and (3) Loop rules for handling loops.

A program rule is a completed definition ¢> +-> B1 V . .. V Bn E Comp(P) used from left to right: ¢> can be rewritten to B1 V ... V Bn. and-.¢> to -.B1 1\ ... 1\ -.Bn. These are called literal rewriting.

A goal, also called a goal formula, is a formula which may involve -., V and /\ . A goal resulted from a literal rewriting from another goal is called a derived goal. Like a formula, a goal may be transformed to another goal without changing its semantics. This is carried out by simplification rules.

We assume that in all goals negation appears only in front of a literal. This can be achieved by simple transformations using the following rules: for any formulas <I> and Ill,

3.1 Simplification rules

The simplification rules constitute a nondeterministic trans­ formation system formulated with a mechanism of loop han­ dling in mind, which requires keeping track of literal se­ quences go, . . . , gn where each gi, 0 < i ::; n, is in the goal formula resulted from rewriting gi-l · Two central mecha­ nisms in formalizing goal rewrite systems are rewrite chains and contexts.

• Rewrite Chain: Suppose a literal l is written by its defi­ nition ¢> +-> <I> where l = ¢> or l = -.¢>. Then, each literal l' in the derived goal is generated in order to prove l. This ancestor-descendant relation is denoted l -< l'. A sequence 11 -< . . . -< ln is then called a rewrite chain, abbreviated as l1 -<+ ln.
• Context: A rewrite chain g = go -< g1 -< .. . -< gn = T records a set of literals C = {go, ... , gn-d for proving g. We will write T( {go, ... , gn-l}) and call C a context. A context will also be used to maintain consistency: if g can be proved via a conjunction, all ofthe conjuncts need be proved with contexts that are non-conflicting with each other. For simplicity, we assume that when­ ever -.F is generated, it is automatically replaced by T( C), where Cis the set of literals on the corresponding rewrite chain, and -.Tis automatically replaced by F .

Note that for any literal in a derived goal, the rewrite chain leading to it from a literal in the given goal is uniquely deter­ mined. As an example, suppose the completion of a program has the definitions: a +-> -.b 1\ -.c and b +-> q V -.p. Then, we get a rewrite sequence, a -+ -.b 1\ -.c -+ -.q 1\ p 1\ -.c. For the three literals in the last goal, we have rewrite chains from a: a -< -.b -< -.q; a -< -.b -< p; and a -< -.c.

Simplification Rules: Let <I> and <I>i be goal formulas, C be a context, and l a literal.

SR3 merges two contexts if they contain no complemen­ tary literals, otherwise SR4 makes it a failure to prove. Re­ peated applications of SRS and SRS' can transform any goal formula to a disjunctive normal form (DNF).

3.2 Loop rules

After a literal l is rewritten, it is possible that at some later stage either l or -.l appears again in a goal on the same rewrite chain. Two rewrite rules are formulated to handle loops.

Definition 3.1 LetS = 11 -<+ ln be a rewrite chain.

• If -.ll = ln or l1 = -.ln. then Sis called an odd loop.
• !fit= ln. then
• S is called a positive loop if l1 and ln are both atoms and each literal on It -<+ ln is also an atom;
• S is called a negative loop if It and ln are both negative literals and each literal on l 1 -<+ ln is also negative;
• Otherwise, S is called an even loop.

In all the cases above, ln is called a loop literal.

Loop Rules: Let g1 --<+ 9n be a rewrite chain.

• LRl. 9n--> F if g; --<+ gn, for some 1 s; i < n, is a positive loop or an odd loop.

A rewrite sequence is a sequence of zero or more rewrite steps Qo --> . .. --> Qk, denoted Qo -->* Qk. such that Qo is an initial goal, and for each 0 s; i < k, Qi+1 is obtained from Q; by

• literal rewriting at a non-loop literal in Q;, or
• applying a simplification rule to a subformula of Q;, or
• applying a loop rule to a loop literal in Q;.

Example 3.2 For the program given in the Introduction, Po= {a+- not b. b +- c, nota. c +-a.}, a is proved but b is not. This is shown by the following rewrite sequences:

3.3 Previous results

In [Lin and You, 2001], it is shown that (1) a goal rewrite sys­ tem is a canonical system, i.e., it confluent and terminating; (2) any goal rewrite system is sound and complete w.r.t. the partial stable model semantics; and (3) the rewriting frame­ work can be extended for abduction in a relatively straight­ forward manner.

4 Goal Rewrite Systems with Computed Rules

We first use two examples to illustrate the main technical re­ sults of this section.

Example 4.1 Given a rewrite system R 0 , suppose we have a rewrite sequence ·q --> a --> a --> F. The failure is due to a positive loop on a. We may recycle the computed answer by replacing the rewrite rule for ·q by the new rule, ·q --> F. We thus get a new system, say R 1 . Suppose in trying to prove g we have

where the last step makes use of the computed answer for ·q. The question arises as whether this way of using previ­ ously computed results guarantees the soundness and com­ pleteness. Theorem 4.6 to be proved later in this paper an­ swers this question positively. To see it for this example, as­ sume we have the following, successful proof in R 0

where the termination is due the even loop on a. Had such a sequence existed, recycling would have produced a wrong result. However, one can see that the existence of the rewrite step a --> ·q implies the existence of a different way to prove ·q:

contradicting that ·q was rewritten to Fin R 0 .

Before giving the next example, we introduce a different way to understand rewrite sequences. Since any goal formula can always be transformed to a DNF using the distributive rules SR5 and SR5', and the order of rewriting does not mat­ ter, we can view rewriting as generating a sequence of DNFs. Thus, a rewrite sequence in DNF from an initial goal g,

can be conveniently represented by derivation trees, or d­ trees, one for each N; representing one possible way of prov­ ing g. For any i, the d-tree for N; has g as its root node, wherein a branch from g to a leaf node corresponds to a rewrite chain from g that eventually ends with an F or some T(C). As such a disjunct is a conjunction, a successful proof requires each branch to succeed and the union of all resulting contexts to be consistent.

The next example is carefully constructed to illustrate that recycling may not yield the same answers as if no recycling were carried out. In particular, one can sometimes get addi­ tional answers.

Example 4.2 Consider the program:

In Fig. 1, each d-tree consists of a single branch. The left two d-trees are expanded from goal p corresponding to the following rewrite sequence:

The next two d-trees are for goal g, corresponding to the rewrite sequence:

Now, we recycle the proof for p in the proof for g and com­ pare it with the one without recycling. Clearly, the successful d-tree for g (the fourth from the left) will still succeed as it doesn't involve any p. The focus is then on the d-tree in the middle, in particular, the node p in it; this d-tree fails when no recycling was performed.

Since pis previously proved with context {g, a, ·b }, recy­ cling of this proof amounts to terminating p with a context which is the union of this context with the rewrite chain lead­ ing to p (see the d-tree on the right). But this results in a successful proof that fails without recycling.

Though recycling appears to have generated a wrong re­ sult, one can verify that both generated contexts, {g, a, ·b} and {g, a, e, p, ·b }, belong to the same partial stable model. Thus, recycling in this example didn 't lead to an incorrect answer but generated a redundant one. Theorem 4.6 shows that this is not incidental. Indeed, if p is true in a partial sta­ ble model, by derivation (look at the d-tree in the middle), so must be e, a, and g.

4.1 Rewrite systems with computed rules

Given a goal rewrite system R, we may denote a rewrite se­ quence from a literal g by g --+ R E.

Definition 4.3 (Computed rule)

Let R be a goal rewrite system in which literal p is rewritten to its normal form. The computed rule for p is defined as: If p --+ R F, the computed rule for p is the rewrite rule p --+ F; ifp--+ R T(C1) V ... V T(Cn), then the computed rule for pis the rewrite rule p--+ T(C1 ) V ... V T(Cn)·

For the purpose of recycling, a computed rule p --+ E is meant to replace the existing literal rewrite rule for p. If a computed rule is of the form p --+ F representing a failed derivation, it can be used directly as the literal rewrite rule for p. Otherwise, we must combine the contexts in E with the rewrite chain leading top, and keep only consistent ones.

Recycling Rule:

Let 91 --<+ 9n be a rewrite chain where 9n is a non-loop lit­ eral. Let G = {g1, ... ,gn}, and 9n--+ T(D1) V ... V T(Dk) be the computed rule for 9n· Further, let { D~, ... , D~,} be the subset of {D1, ... , Dk} containing any Di such that DiU G is consistent. Then, the recycling rule for 9n is defined as:

In the sequel, a rewrite system includes the recycling rule as well as zero or more computed rules. We note that the termination and confluence properties remain to hold for the extended systems.

We are interested in the soundness and completeness of a series of rewrite systems, each of which recycles computed answers generated on the previous one. For this purpose, given a program P we use Rfj, to denote the original goal rewrite system where literal rewrite rules are defined by the Clark completion of P. For all i ~ 0, R1 1 is defined in terms of R~ as follows: Let ~i be the set of computed rules (generated) on R~ for the set of literals Lt::.; Then, R1 1 is the rewrite system obtained from R~ by replacing the rewrite rules for the literals in 12t::., by those in ~i· In the rest of this sectin, we will always refer to a fixed program P. Thus we may drop the subscript P and write Ri.

Definition 4.4 A rewrite system Ri is sound iff, for any literal g and rewrite sequence g--+ R' T(C1) V ... V T(Cn), and for each Cj, j E [l..n], there exists a partial stable model M of P such that g E CJ s;; M. Ri is complete iff, for any literal g such that g E M for some partial stable model M of P, there is a rewrite sequence g -+R' T(CI) V ... V T(Cn) such that for some Cj, j E [l..n], g E Cj s;; M.

An important property of provability by rewriting is the so-called loop rotation, which is needed in order to prove the completeness of recycling; namely, a proof (a successful branch in ad-tree) terminated by a loop rule can be captured in rotated forms.

To describe this property, we need the following notation about rewrite chains: Any direct dependency relation l --< l' may be denoted by l · l', and we allow a segment (which may be empty) of a rewrite chain to be denoted by a Greek letter such as 6, e, and~· Thus, we may write x · 6 · y to denote a rewrite chain from x toy via 6, or x · 6 to mean a rewrite chain that begins with x followed by the segment denoted by 6. A rewrite chain may also be used to denote the set of the literals on it.

Lemma 4.5 (loop rotation)

Let R 0 be a rewrite system without computed rules. Let Tr be a d-treefor literal g that succeeds with context C. Suppose a branch ofTr ends with a loop, g · 0 · g, for some 0. Then, for any literall E 0, there is a proof of l that succeeds with the same context C.

Proof A loop, 1r = g · h · l 2 · . . . · ln · g, where g and l; are literals, can always be rotated as

and so on, so that if 1r is a negative loop (or an even loop, resp.) so is its rotated loop. Rotation over a d-tree can be performed as follows: remove the top node n, and for any link from the top node, n · q, attach the link n · q to any occurrence of n. The assumption of the existence of loop g · e · g ensures that in every round of rotation there is at least one occurrence of the top node. (See Fig 2 for an illustration where rotation proceeds from left to right.) It can be seen that the type of a loop is always preserved and the set of literals on the tree remains unchanged. 0

4.2 Soundness and completeness of recycling

Theorem 4.6 For any i ~ 0, Ri is sound and complete.

We sketch how this can be proved. We can prove the claim by induction on i. R 0 , the system without computed rules, is sound and complete [Lin and You, 2001]. Now assume for all j with 0 :::; j :::; i, R1 are sound and complete, and show that R'+l is also sound and complete.

We only need to consider the situations where rewriting in R'+ 1 differs from that of Ri. Let .Ce:.. , be the set of literals whose computed rules are generated on Ri . We can first carry out rewriting without rewriting the literals that are in .Ce:.. .. In this case, rewriting from g in both Ri and Ri+ 1 terminate at the same expression, which is either F or a DNF, say N1 v ... V Nm. Each Ni can be represented by ad-tree.

For the soundness, we assume g ---> R'+l T(D1) V ... v T(D8 ). For any D E {D1 , ... , D8 }, we need to show that there is a partial stable model M such that D <::;; M. Consider the d-tree Tr that generates D and suppose g is its root node. We can show inductively in a bottom-up fashion that all the literals on Tr belong to the same partial stable model.

For the completeness, we can show that for any context generated in R', the same context will be generated in Ri+ 1 . Then, R'+l is complete simply because Ri is complete.

Let p E .Ce:.. , , and consider a proof of g in Ri that goes through p. In particular, consider a d-tree of this proof that contains p. Since each branch of this d-tree can be expanded and eventually terminated independent of others, for simplic­ ity, we consider how a branch g ·~·pin the d-tree is extended. In Ri+ 1 the computed rule for pis used while in Ri it is not. We only need to consider two cases in Ri: either g is proved via p and a previously computed rule, or the branch is termi­ nated due to a loop. Here, let us consider the latter only. In expanding the rewrite chain g · ~ · p in Ri, we may form a loop, say g . ~ . p . e. If the loop is in e' exactly the same loop occurs in rewriting p as the top goal in Ri, so it is part of the computed rule for p. Otherwise it is a loop that crosses over p, in the general form

where l is the loop literal. As a special case of loop rotation over a branch (cf. Lemma 4.1), the same way of terminating a rewrite chain presents itself in proving p as the top goal in R', which is

If the loop on 1r is a negative loop (or an even loop, resp.), so is 1r'. Thus the same context will be generated in Ri+ 1 .

As given in the corollary below, if we only recycle failed proofs then exactly the same contexts will be generated.

Corollary 4.7 Let Ri be a rewrite system where each com­ puted rule is of the form p ---> F. Let g be a literal and E be a normal form. Then, for any i 2=': 0, g ---> Ro E iff g ---> R' E.

5 Recycling in Abductive Rewrite Systems

As shown in [Lin and You, 2001], the rewriting framework can be extended to abduction in a straightforward way: the only difference in the extended framework is that we do not apply the Clark completion to abducibles. That is, once an abducible appears in a goal, it will remain there unless it is eliminated by the simplification rule SR2 or SR2'. In a sim­ ilar way, the goal rewrite systems with computed rules in the previous section can be extended to abduction as well. Once a goal is rewritten to a disjunction of conjunctions of abducible literals and T:

where each lij is either T or an abducible literal, and Ci1 u · · · U Cik, is consistent for each i, then this result can be re­ cycled .

6 Experiments

We have implemented a depth-first search rewrite procedure with branch and bound. The procedure can be used to com­ pute explanations using a nonground program, under the con­ dition that in each rule a variable that appears in the body must also appear in the head. When this condition is not sat­ isfied, one only needs to instantiate those variables that only appear in the body of a rule. This is a significant departure from the approaches that are based on ground computation where a function-free program is first instantiated to a ground program with which the intended models are then computed.

To check the effectiveness of the idea of recycling, we tested our system on the logistics problem in [Lin and You, 2001]. This is a domain in which there is a truck and a pack­ age. A package can be in or outside a truck, and a truck can be moved from one location to another. The problem is that given state constraints such as that the truck and the pack­ age can each be at only one location at any given time, and that if the package is in the truck, then when the truck moves to a new location, so does the package, how we can derive a complete specification of the effects of the action of moving a truck from one location to another. Suppose that we have the following propositions: ta(x) (pa(x)) - the truck (package) is at location x initially; in- the package is in the truck initially; ta(x, y, z ) (pa(x, y, z))- the truck (package) is at location x after performing the action of moving it from y to z; in(y, z)­ the package is in the truck after performing the action of mov­ ing the truck from y to z. Then in [Lin and You, 2001], the problem is solved by computing the abduction of successor state propositions {ta(x,y,z), pa(x,y,z), in(y, z)} in terms of initial state propositions { ta(x), pa(x ), in} (abducibles) us­ ing the following logic program (see [Lin and You, 2001] for more details):

Here the variables are to be instantiated over a domain of locations. For instance, given query pa(3, 2, 3) , our system would compute its abduction as pa(3) V in, meaning that for it to be true, either the package was initially at 3 or it was inside the truck.

Which subgoals to compute first? If we want to compute the abduction of all propositions, without the framework of recycling introduced here, the only way is to compute them one by one independently. With the idea of recycling, we can try to recycle previously computed results. The question is then which goals to compute first. This question arises even if we just want to compute the abduction of a single goal: instead of computing it using the original program, it may sometimes be better if we first compute the abduction of some other goals and recycle the result.

A simple solution is to find out the dependency relations among the propositions: a proposition p depends on q if ei­ ther q is in the body of a rule whose head is p or inductively, there is another proposition r such that p depends on r, and r depends on q.

For our program above, it is easy to see that among the propositions that we want to compute their abduction of, those of the form in(X, Y) and those of the form ta(X, Y, Z) are independent of each other, but those of the form pa(X, Y, Z) are depended on propositions of the forms in(X, Y) and ta(X, Y, Z) . So we should compute first the ab­ duction ofin(X, Y) and ta(X, Y, Z) . Now in(X, Y) is solved by rule (8), ta(X, Y, X) by rule (2), and as it turned out, when X =1- Z, ta(X, Y, Z) is always false, and its computation is relatively easy. For instance, for the domain with 9 locations, query ta(7, 1, 6) took only 2.6 seconds. In comparison, query pa(7, 1, 7) took more than 7000 seconds without recycling.

Table 1 contains run time data for some representative queries. 1 For comparison purpose, each query is given two entries: the one under "NR" refers to regular rewriting sys­ tem without using recycling, and the one under "WR" refers to rewriting system using computed rules about ta(X, Y, Z). As one can see, especially for hard queries like pa(7, 1, 7), re­ cycling in this case significantly speeds up the computation.

7 Concluding remarks

We have considered the problem of how to reuse previously computed results for answering other queries in the abductive rewriting system of Lin and You [2001] for logic programs with negation, and showed that this can indeed be done. We have also described a methodology of using the recycling system in practice by analysing the dependency relationship among propositions in a logic programs. We applied this methodology to the problem of computing the effect of ac­ tions in a logistics domain, the same one considered in [Lin and You, 2001], and our experimental results showed that re­ cycling in this domain can indeed result in good performance gain. For future work we want to implement a system that can automatically analyse a program and decide how best to recycle previous computations.

1 Our implementation was written in Sicstus Pro log, and the ex­ periments were done on a Pili 1GHz notebook with 512MB mem­ ory. For generating explanations for regular rewriting system, our implementation is a significant improvement over the one in [Lin and You, 20011. For instance, for a domain with 7 locations query pa(3, 2, 3) took more than 20 minutes for the implementation re­ ported in [Lin and You, 2001], but required less than 1 second under our implementation running on a comparable machine.