Abduction in Logic Programming: A New Definition and an Abductive Procedure Based on Rewriting

1 Abduction in logic programming

In general, given a background theory a0 , and an observation ✁ to explain, an abduction of ✁ w.r.t. a0 is a theory ✂ such that ✂ ✄ a0 ✆ ✞ ✁ . Normally, we want to put some additional conditions on ✂ , such as that it is consistent with a0 and contains only those propositions called abducibles. For instance, in propositional logic, given a background theory a0 , a set ✟ of assumptions or abducibles, and a proposition ✁ , an explanation ✠ of ✁ is commonly defined (see [Reiter and de Kleer, 1987], [Poole, 1988], and [Konolige, 1992]) to be a minimal set of literals over ✟ such that a0 ✄ ✠ ✆ ✞ ✁ and a0 ✄ ✠ is consistent.

In the context of logic programming, abduction has been investigated from both proof-theoretic and model-theoretic perspectives (e.g. [Eshghi and Kowalski, 1989; Kakas and Mancarella, 1990; Satoh and Iwayama, 1992]). One of the most influential definitions of abduction in logic programming is that of Kakas and Mancarella's generalized stable model semantics [1990]. Given a logic program ☛ , a set ✟ of atoms standing for abducibles, and a query ✁ , Kakas and Mancarella define an abductive explanation ✠ to be a subset of ✟ such that there is an answer set (also called a stable model) ☞ of ☛ ✄ ✠ that satisfies ✁ .

One can see the following two differences between this definition and the one that we defined above for propositional logic: In propositional logic, ✠ is a set of literals, but in logic programming, it is just a set of atoms; In propositional logic, ✠ must be minimal, in terms of the subset ordering relation; but there is no such requirement in the case of logic programming.

Jia-Huai You

Department of Computing Science University of Alberta

Edmonton, Alberta, Canada T6G 2H1

One could argue that these differences are due to the fact that under the answer set semantics, negation is considered to be "negation-as-failure." If none of the atoms in ✟ appear in the head of a rule in the logic program ☛ , then adding a set ✠ ✎ ✟ to ☛ really means that we are adding the complete literal set, ✠ ✄ ✑ ✓ ✕ ✆ ✕ ✗ ✟ ✚ ✕ ✢ ✗ ✠ ✤ , to ☛ . This would also explain why there is no minimality condition in the definition: two complete sets of literals are never comparable in terms of the subset relation.

However, while this notion of abductive explanations makes sense in theory, it is problematic in practice. For instance, if ✟ ✞ ✑ ✦ ✚ ★ ✤ , and ☛ ✞ ✑ ✁ ✫ ✦ ✭ ✤ , then there are two abductive explanations for ✁ according to Kakas and Mancarella's definition: ✑ ✦ ✤ and ✑ ✦ ✚ ★ ✤ . In general, if ✟ has ✰ elements, then there are ✱ ✲ ✴ ✶ abductive explanations for ✁ , a number that is too big to manage.

Since in this case ✦ is the explanation that we are looking for, it is tempting here to say that we should prefer minimal abductive explanations like what we did for propositional logic. As we mentioned above, this does not make sense if we take an abductive explanation to be a complete set of literals as implied by the answer set semantics. However, one can still try to minimize the set of atoms, in this case, preferring ✑ ✦ ✤ over ✑ ✦ ✚ ★ ✤ .

However, this minimization strategy is problematic when a program contains negation. Consider a situation in which a boat can be used to cross a river if it is not leaking or, if it is leaking, there is a bucket available to scoop the water out of the boat. This can be axiomatized by the following logic program ☛ :

✸ ✦ ✰ ✺ ✼ ✾ ❀ ❀ ✫ ★ ✾ ✦ ❃ ✚ ❅ ❇ ❈ ❊ ❋ ✦ ❍ ■ ✰ ▲ ✭ ✸ ✦ ✰ ✺ ✼ ✾ ❀ ❀ ✫ ★ ✾ ✦ ❃ ✚ ❊ ❋ ✦ ❍ ■ ✰ ▲ ✚ ❖ ✦ ❀ ◗ ❘ ✸ ❍ ❋ ❃ ✭

Now suppose that we saw someone crossed the river, how do we explain that? Clearly, there are two possible explanations: either the boat is not leaking or the person has a bucket with her. In terms of Kakas and Mancarella's definition, there are three abductive explanations for ✸ ✦ ✰ ✺ ✼ ✾ ❀ ❀ , ✑ ★ ✾ ✦ ❃ ✤ , ✑ ★ ✾ ✦ ❃ ✚ ❖ ✦ ❀ ◗ ❘ ✸ ❍ ❋ ❃ ✤ , and ✑ ★ ✾ ✦ ❃ ✚ ❊ ❋ ✦ ❍ ■ ✰ ▲ ✚ ❖ ✦ ❀ ◗ ❘ ✸ ❍ ❋ ❃ ✤ , assuming that ✟ ✞ ✑ ★ ✾ ✦ ❃ ✚ ❊ ❋ ✦ ❍ ■ ✰ ▲ ✚ ❖ ✦ ❀ ◗ ❘ ✸ ❍ ❋ ❃ ✤ is the set of abducibles. But only one of them, ✑ ★ ✾ ✦ ❃ ✤ , is minimal.

On a closer look, we see that in our first example, when we say that ✑ ✦ ✤ is a preferred explanation over all the others, we do not mean the complete set of literals ✑ ✦ ✚ ✓ ★ ✤ , is preferred over all the others. While we want ✦ to be part of the explanation, we don't necessarily want ✓ ★ because we do not want to apply negation as failure on abducibles, which are assumptions one can make one way or the other. What we want is for the set ✑ ✦ ✤ itself to be the best explanation for ✁ .

One way to justify this is that all possible ways of completing this set into a complete set of literals, ✑ ✦ ✚ ✓ ★ ✤ and ✑ ✦ ✚ ★ ✤ , turn out to correspond to all the abductive explanations of ✁ according to Kakas and Mancarella's definition. The same kind of justification turns out to work for our second example as well: the reason that ✑ ★ ✾ ✦ ❃ ✤ is not a preferred explanation is that while its completion according to negation-as-failure, ✑ ★ ✾ ✦ ❃ ✚ ✓ ❊ ❋ ✦ ❍ ■ ✰ ▲ ✚ ✓ ❖ ✦ ❀ ◗ ❘ ✸ ❍ ❋ ❃ ✤ is an explanation, some of its other completions, for example ✑ ★ ✾ ✦ ❃ ✚ ❊ ❋ ✦ ❍ ■ ✰ ▲ ✚ ✓ ❖ ✦ ❀ ◗ ❘ ✸ ❍ ❋ ❃ ✤ is not an explanation. This motivates our following definitions.

2 Abduction in logic programming revisited

In this paper, we consider (normal) logic programs which are sets of rules of the form

where ✦ , ★ ✂ and ✸ ✂ are atoms of the underlying propositional language ☎ . Here "❅ ❇ ❈ " is the so-called default negation, and defined according to the answer set semantics [Gelfond and Lifschitz, 1988].

Let ☛ be a logic program, ✟ a set of propositions standing for abducibles, and ✁ a proposition. In the following, without loss of generality, we shall assume that none of the abducibles in ✟ occur in the head of a rule in ☛ . 1

In the following, by a hypothesis ✆ we mean a consistent set of literals over ✟ , i.e. it is not the case that ✕ and ✓ ✕ are both in ✆ for some ✕ ✗ ✟ . We say that a hypothesis is complete if for each atom ✕ ✗ ✟ , either ✕ or ✓ ✕ is in ✆ , but not both. Notice that a complete hypothesis is really a truth-value assignment over the language ✟ . We say that a hypothesis ✆ is an extension of another one ✝ if ✝ ✎ ✆ , and a complete extension is an extension that is complete.

Definition 2.1 A complete hypothesis ✆ is said to be an explanation of ✁ w.r.t. ☛ and ✟ iff there is an answer set ☞ of ☛ ✄ ✆ ✠ such that ☞ contains ✁ and for any ✓ ✕ ✗ ✆ , ✕ ✢ ✗ ☞ , where ✆ ✠ is the set of atoms in ✆ .

Definition 2.2 A hypothesis is said to be an explanation of ✁ iff every complete extension of it is an explanation. A hypothesis ✆ is said to be a minimal explanation if it is an explanation, and there is no other explanation ✆ ✌ such that ✆ ✌ ✏ ✆ .

Consider the logic program ☛ in the previous section about ✸ ✦ ✰ ✺ ✼ ✾ ❀ ❀ . The following are the complete hypotheses that explain ✸ ✦ ✰ ✺ ✼ ✾ ❀ ❀ :

✑ ★ ✾ ✦ ❃ ✚ ✓ ❊ ❋ ✦ ❍ ■ ✰ ▲ ✚ ❖ ✦ ❀ ◗ ❘ ✸ ❍ ❋ ❃ ✤ ✚ ✑ ★ ✾ ✦ ❃ ✚ ❊ ❋ ✦ ❍ ■ ✰ ▲ ✚ ❖ ✦ ❀ ◗ ❘ ✸ ❍ ❋ ❃ ✤ ✭

Now consider ✑ ★ ✾ ✦ ❃ ✚ ❖ ✦ ❀ ◗ ❘ ✸ ❍ ❋ ❃ ✤ . Clearly every complete extension of this set is an explanation, so it is an explanation as well. Furthermore, it is a minimal explanation as none of its element can be deleted for it continue to be an explanation. Similarly, ✑ ★ ✾ ✦ ❃ ✚ ✓ ❊ ❋ ✦ ❍ ■ ✰ ▲ ✤ is also a minimal explanation.

1 If ✓ ✔ ✖ occurs in the head of a rule, then we can always introduce a new proposition, say ✓ ✗ , add the rule ✓ ✙ ✓ ✗ to ✢ , add ✓ ✗ to ✖ and delete ✓ from ✖ .

If we take a hypothesis to be the conjunction of its elements, then we have that in the propositional logic,

where ✯ ✶ is the set of all complete hypotheses that are explanations of ✁ , ✯ ✰ the set of all explanations of ✁ , and ✯ ✱ the set of all minimal explanations of ✁ . Therefore the set of minimal explanations is a succinct representation of the set of all explanations.

It is clear from our definition that a complete hypothesis ✆ is an explanation of ✁ iff ✆ ✠ is an abductive explanation of ✁ according to Kakas and Mancarella's definition. This implies that if none of the abducibles occur in the head of any clauses in ☛ , then

where ✯ ✶ is the set of all abductive explanation of ✁ according to Kakas andMancarella's definition, ✸ ❊ ✳ ✠ ✵ ✞ ✠ ✄ ✑ ✓ ✕ ✆ ✕ ✗ ✟ ✚ ✕ ✢ ✗ ✠ ✤ , and ✯ ✰ is the set of all minimal explanations of ✁ .

So in a sense, the set of Kakas and Mancarella's abductive explanations and that of our minimal explanations are equivalent. However, as we have seen above, the number of abductive explanations can be very large. Enumerating them all is impossible even in simple, small domains. In contrast, the number of minimal explanations are much smaller. More importantly, just like explanations in propositional logic, they only include "relevant propositions."

But computationally, it may be hard to compute minimal explanations from scratch. It is often easier to compute first a small "cover" of all explanations.

Definition 2.3 A set ✯ of hypotheses is said to be a cover of ✁ w.r.t. ☛ and ✟ iff

where ✯ ✸ is the set of minimal explanations of ✁ .

Proposition 2.4 If ✯ is a cover of ✁ , then each ✆ ✗ ✯ must be an explanation of ✁ .

So a cover is a set of explanations such that any complete explanation must be an extension of one of the explanations in the cover. Once we have a cover, then we can find all minimal explanations by propositional reasoning alone. Recall that a conjunction of literals ✆ is a prime implicant of a formula ✺ if ✆ ✆ ✞ ✺ , and there is no other ✝ such that ✝ ✆ ✞ ✺ and ✝ is a subset of ✆ , i.e. ✆ is a minimal conjunction of literals that entails ✺ .

Proposition 2.5 Let ✯ be a cover of ✁ . Then a hypothesis is a minimal explanationof ✁ iff it is a prime implicant of ✻ ✤ ✥ ✦ ✆ .

In the rest of this paper, we shall propose a rewriting system for generating explanations of a proposition in a logic program. We shall first define it for logic programs without abducibles. We will then extend the system to logic programs with abducibles, and show that for any query, the rewriting system generates an approximation of a cover set in the general case, and exactly a cover set when the given logic program has no so-called "odd loops." We will then discuss an application of our system to reasoning about actions and present some experimental results.

3 Goal Rewrite Systems

Given a (ground) program ☛ , the Clark completion of ☛ , denoted ✺ ✾ a0 ✕ ✳ ☛ ✵ , is the following set of equivalences: for each atom ✂ ✗ ☎ ,

• ✄ if ✂ does not appear as the head of any rule in ☛ , ✂ ☎ ✝ ✗ ✺ ✾ a0 ✕ ✳ ☛ ✵ .
• ✄ otherwise, ✂ ☎ ◗ ✶ ✟ ✭ ✭ ✭ ✟ ◗ ✲ ✗ ✺ ✾ a0 ✕ ✳ ☛ ✵ (with default negations replaced by negative literals), if there are exactly ✰ rules ✂ ✫ ◗ ✂ ✗ ☛ with ✂ as the head. We write a0 for ◗ ✂ if ◗ ✂ is empty.

The idea of goal rewriting is simple. A completed definition ✂ ☎ ◗ ✶ ✟ ✭ ✭ ✭ ✟ ◗ ✲ ✗ ✺ ✾ a0 ✕ ✳ ☛ ✵ can be used as a rewrite rule from left to right: ✂ is rewritten to ◗ ✶ ✟ ✭ ✭ ✭ ✟ ◗ ✲ , and ✓ ✂ to ✓ ◗ ✶ ✌ ✭ ✭ ✭ ✌ ✓ ◗ ✲ . We call these literal rewriting, and the completed definitions program (rewrite) rules.

A goal is a formula which may involve ✓ , ✟ and ✌ . A goal is also referred to as a goal formula. A goal resulted from a literal rewriting from another goal is called a derived goal. A goal with negation appearing only in front of atoms is said to be signed, a term introduced in [Kunen, 1989] for a similar purpose. For convenience, we assume that all goals are signed, which can be achieved easily by simple transformations using the following rules: for any formulas ✎ and ✏ ,

Like a formula, a goal may be further transformed to a suitable form for literal rewriting without changing its semantics. With amechanismof loop handling, rewriting of a goal ✕ terminates at either a0 meaning that ✕ is proved, or ✝ meaning that ✕ is not proved. Hence, a goal rewrite system consists of three types of rewrite rules: (i) program rules from ✺ ✾ a0 ✕ ✳ ☛ ✵ for literal rewriting, (ii) simplification rules to transform and simplify goals, and (iii) loop rules for handling loops.

3.1 Simplification rules

The simplification subsystem is formulated with a mechanism of loop handling in mind, which requires keeping track of literal sequences ▲ ✸ ✚ ✭ ✭ ✭ ✚ ▲ ✲ where each ▲ ✂ , ✖ ✗ ■ ✙ ✰ , is in the goal formula resulted from rewriting ▲ ✂ ✴ ✶ . Two central mechanisms in formalizing goal rewrite systems are rewrite chains and contexts.

• ✄ Rewrite Chain: Suppose a literal ❊ is written by its definition ✂ ☎ ✎ where ❊ ✞ ✂ or ❊ ✞ ✓ ✂ . Then, each literal ❊ ✌ in the derived goal is generated in order to prove ❊ . This ancestor-descendant relation is denoted ❊ ✛ ❊ ✌ . A sequence ❊ ✶ ✛ ✭ ✭ ✭ ✛ ❊ ✲ is then called a rewrite chain, abbreviated as ❊ ✶ ✛ ✠ ❊ ✲ . Notice that it is essential here that any goal ✣ be in the form of a signed goal, and that when ✓ ✕ is in ✣ , we have that ❊ ✛ ✓ ✕ but not ❊ ✛ ✕ .
• ✄ Context: A rewrite chain ▲ ✞ ▲ ✸ ✛ ▲ ✶ ✛ ✭ ✭ ✭ ✛ ▲ ✲ ✞ a0 records a set of literals ✺ ✞ ✑ ▲ ✸ ✚ ✭ ✭ ✭ ✚ ▲ ✲ ✴ ✶ ✤ for proving ▲ . We will write a0 ✳ ✑ ▲ ✸ ✚ ✭ ✭ ✭ ✚ ▲ ✲ ✴ ✶ ✤ ✵ and call ✺ a context. For simplicity, we assume that whenever ✓ ✝ is generated, it is automatically replaced by a0 ✳ ✺ ✵ , where ✺ is the set of literals on the corresponding rewrite chain, and ✓ a0 is automatically replaced by ✝ .

Note that for every literal in any derived goal, the rewrite chain leading to it from a literal in the given goal is uniquely determined. As an example, suppose the completion of a program is: ✑ ✦ ☎ ✓ ★ ✌ ✓ ✸ , ★ ☎ ✁ ✟ ✓ ✕ ✤ . We then have a rewrite sequence ✦ ✑ ✓ ★ ✌ ✓ ✸ ✑ ✓ ✁ ✌ ✕ ✌ ✓ ✸ . For the three literals in the last goal, we have the following rewrite chains for them from ✦ : ✦ ✛ ✓ ★ ✛ ✓ ✁ , ✦ ✛ ✓ ★ ✛ ✕ , and ✦ ✛ ✓ ✸ .

Simplification Rules:

Let ✎ ✂ 's be any goal formulas, ✺ a context, and ❊ a literal.

The simplification system is a nondeterministic transformation system. The primed version of a rule is its symmetric case. Most of the rules are about the logical equivalence between the two sides of a rule. SR3 merges two contexts if they are consistent, otherwise SR4 makes it a failure to prove. SR5 and SR5' prevent generating an inconsistent context before literal ❊ is even proved.

Note that the proof-theoretic meaning of a goal formula may not be the same as the logical meaning of the formula. E.g., the goal formula ✦ ✟ ✓ ✦ (a tautology in classic logic) could well lead to an ✝ if neither ✦ nor ✓ ✦ can be proved.

For goal rewriting that does not involve loops, the system described so far is sufficient.

Example 3.1 Let ☛ be

Then ✺ ✾ a0 ✕ ✳ ☛ ✵ is:

The rewrite sequence below is generated by focusing on the left part of a goal.

• ▲ ✑ ✓ ✦ ✑ ✳ ★ ✟ ✸ ✵ ✌ ✳ ✓ ★ ✟ ✲ ✵ ✑ ✳ ✁ ✟ ✓ ✕ ✟ ✸ ✵ ✌ ✳ ✓ ★ ✟ ✲ ✵ ✑ ✳ ✝ ✟ ✓ ✕ ✟ ✸ ✵ ✌ ✳ ✓ ★ ✟ ✲ ✵ ✑ ✳ ✓ ✕ ✟ ✸ ✵ ✌ ✳ ✓ ★ ✟ ✲ ✵ ✑ ✳ a0 ✳ ✺ ✵ ✟ ✸ ✵ ✌ ✳ ✓ ★ ✟ ✲ ✵ where ✺ ✞ ✑ ▲ ✚ ✓ ✦ ✚ ★ ✚ ✓ ✕ ✤ ✑ ✳ a0 ✳ ✺ ✵ ✌ ✳ ✓ ★ ✟ ✲ ✵ ✵ ✟ ✳ ✸ ✌ ✳ ✓ ★ ✟ ✲ ✵ ✵ ✑ ✳ a0 ✳ ✺ ✵ ✌ ✓ ★ ✵ ✟ ✳ a0 ✳ ✺ ✵ ✌ ✲ ✵ ✟ ✳ ✸ ✌ ✳ ✓ ★ ✟ ✲ ✵ ✵ %a0 ✁ ✁ ☎ ✆ ✞ ✠ ☛ ✑ ✝ ✟ ✳ a0 ✳ ✺ ✵ ✌ ✲ ✵ ✟ ✳ ✸ ✌ ✳ ✓ ★ ✟ ✲ ✵ ✵ ✑ ✳ a0 ✳ ✺ ✵ ✌ ✲ ✵ ✟ ✳ ✸ ✌ ✳ ✓ ★ ✟ ✲ ✵ ✵ ✑ ✳ a0 ✳ ✺ ✵ ✌ ✝ ✵ ✟ ✳ ✸ ✌ ✳ ✓ ★ ✟ ✲ ✵ ✵ ✑ ✝ ✟ ✳ ✸ ✌ ✳ ✓ ★ ✟ ✲ ✵ ✵
• ✑ ✸ ✌ ✳ ✓ ★ ✟ ✲ ✵ ✑ ✝ ✌ ✳ ✓ ★ ✟ ✲ ✵ ✑ ✝

3.2 Loop rules

After a literal ❊ is rewritten, it is possible that at some later stage either ❊ or ✓ ❊ appears again in a goal on the same rewrite chain. Thus, a loop is a rewrite chain ✑ ❊ ✶ ✚ ✭ ✭ ✭ ✚ ❊ ✲ ✤ such that ❊ ✶ ✞ ❊ ✲ , or ❊ ✶ ✞ ✓ ❊ ✲ . A loop analysis involves classifying all the cases of loops, and for each one, determining the outcome of a rewrite according the underlying semantics. For the problem at hand, there are only four cases.

Definition 3.2 Let ✠ ✞ ❊ ✶ ✛ ✠ ❊ ✲ be a rewrite chain.

• ✄ If ✓ ❊ ✶ ✞ ❊ ✲ or ❊ ✶ ✞ ✓ ❊ ✲ , then ✠ is called an odd loop.
• ✄ If ❊ ✶ ✞ ❊ ✲ , then
• ✠ is called a positive loop if ❊ ✶ and ❊ ✲ are both atoms and each literal on ❊ ✶ ✛ ✠ ❊ ✲ is also an atom;
• ✠ is called a negative loop if ❊ ✶ and ❊ ✲ are both negative literals and each literal on ❊ ✶ ✛ ✠ ❊ ✲ is also negative;
• Otherwise, ✠ is called an even loop.

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

Note that when ❊ ✶ ✞ ❊ ✲ , and all of ❊ ✂ , ✌ ✙ ■ ✙ ✰ , have the same sign, this sign is either positive or negative, though both types of loops are caused by "positive loops" in the given program. These two types of loops must be treated differently according to the semantics.

It turns out that we only need two rewrite rules to handle all four cases.

Loop Rules: Let ▲ ✶ ✛ ✠ ▲ ✲ be a rewrite chain.

LR1. ▲

✲

✑

✝

if ▲ ✂ ✛ ✠ ▲ ✲ , for some ✌ ✙ ■ ✗ ✰ , is a positive loop or an odd loop.

Apparently, a loop literal should always be rewritten by a loop rule.

Example 3.3 ☛ ✶ ✞ ✑ ★ ✫ ❅ ❇ ❈ ✸ ✰ ✸ ✫ ✸ ✤ . Below, ★ is proved and ✓ ★ is not.

☛ ✰ ✞ ✑ ✲ ✫ ❅ ❇ ❈ ✦ ✰ ✦ ✫ ❅ ❇ ❈ ★ ✰ ★ ✫ ❅ ❇ ❈ ✦ ✤ . Both ✲ and ✓ ✲ can be proved.

☛ ✱ ✞ ✑ ✦ ✫ ❅ ❇ ❈ ★ ✰ ★ ✫ ❅ ❇ ❈ ★ ✤ . Neither ✦ nor ✓ ✦ is proved:

3.3 Goal rewrite systems and their properties

To summarize, a rewrite sequence is a sequence of zero or more rewrite steps ✕ ✸ ✑ ✭ ✭ ✭ ✑ ✕ ✍ (denoted ✕ ✸ ✑ ✏ ✕ ✍ ) such that ✕ ✸ is an initial goal (one involving no context), and for each ✖ ✙ ■ ✗ ❍ , ✕ ✂ ✠ ✶ is obtained from ✕ ✂ by

• ✄ literal rewriting at a non-loop literal in ✕ ✂ ; or
• ✄ applying a simplification rule to a subformula in ✕ ✂ ; or
• ✄ applying a loop rule to a loop literal in ✕ ✂ .

We may call a subsequence ✕ ✂ ✑ ✏ ✕ ✍ a rewrite sequence in the understanding that it is part of some rewrite sequence ✕ ✸ ✑ ✏ ✕ ✂ ✑ ✏ ✕ ✍ from an initial goal ✕ ✸ .

Definition 3.4 A goal rewrite system is a triple ✒ ✓ ✕ ✚ ✗ ✙ ✚ ✑ ✛ , where ✓ ✕ is the set of all goals, ✗ ✙ is a set of rewrite rules which consists of program rules from ✺ ✾ a0 ✕ ✳ ☛ ✵ , the simplification rules, and the loop rules; and ✑ is the set of all rewrite sequences.

Goal rewrite systems are like term rewrite systems (see, e.g., [Dershowitz and Jouannaud, 1990]) everywhere except at terminating steps: a terminating step at a subgoal may depend on the history of rewriting.

Two desirable properties of rewrite systems are the properties of termination and confluence. Rewrite systems that possess both of these properties are called canonical systems. A canonical system guarantees that the final result of rewriting from any given goal is unique, independent of any order of rewriting. It therefore allows an implementation to be based on any particular order of rewriting.

Since the simplification system is terminating and literal rewriting only generates non-repeated rewrite chains, it is clear that a goal rewrite system is terminating when the given program is finite. A goal is called a normal form if it cannot be rewritten by any rule.

Proposition 3.5 Let ✒ ✓ ✕ ✚ ✗ ✙ ✚ ✑ ✛ be a goal rewrite system. If ☛ is finite then every rewrite sequence in ✑ is finite. Further, for any rewrite sequence ✕ ✸ ✑ ✏ ✕ ✍ , if ✕ ✍ is a normal form, then either ✕ ✍ ✞ ✝ or ✕ ✍ ✞ a0 ✳ ✺ ✶ ✵ ✟ ✭ ✭ ✭ ✟ a0 ✳ ✺ ✁ ✵ for some a0 ✣ ✌ .

Definition 3.6 Agoal rewrite system ✒ ✓ ✕ ✚ ✗ ✙ ✚ ✑ ✛ is confluent iff for any rewrite sequences ❃ ✶ ✑ ✏ ❃ ✰ and ❃ ✶ ✑ ✏ ❃ ✱ , there exist ❃ ✦ ✗ ✓ ✕ and rewrite sequences ❃ ✰ ✑ ✏ ❃ ✦ and ❃ ✱ ✑ ✏ ❃ ✦ .

Theorem 3.7 Any goal rewrite system ✒ ✓ ✕ ✚ ✗ ✙ ✚ ✑ ✛ with a finite ☛ is confluent.

The goal rewrite systems described here are sound and complete w.r.t. partial stable models. These results are special cases of those for the rewrite systems for abduction given in the next section.

4 Rewrite systems for abduction

Let ☛ be a program and ✟ a set of abducibles. An abducible literals is either an abducible ✂ or its negative counterpart ✓ ✂ .

The rewriting framework that we defined earlier can be extended for 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 ✠ a0 ✱ or ✠ a0 ✱ ✌ .

Just like a rewrite to a0 is written as a0 ✳ ✺ ✵ , where ✺ is the underlying rewrite chain (cf. Section 4.1), a rewrite to an abducible literal ❊ will be written as ❊ ✳ ✺ ✵ for rewrite chain ✺ .

In the following we shall denote by ✒ ✓ ✕ ✚ ✗ ✙ ✚ ✟ ✚ ✑ ✛ the rewrite system obtained by the logic program ☛ and the set ✟ of abducibles. We shall show that it is both sound and complete w.r.t. the partial stable models semantics [Przymusinski, 1990], which is a three-valued generalization of answer set semantics. An answer set of ☛ is also its partial stable model. But sometimes ☛ may not have any answer sets. For instance, if ☛ ✞ ✑ ✕ ✫ ❅ ❇ ❈ ✕ ✰ ✁ ✫ ✤ , then ☛ has no answer set, because there is no way to assign a truth value to ✕ . However, ☛ has a partial stable model in which ✁ is true and ✕ is undefined. The following definition is adopted from [You and Yuan, 1995].

Let ☛ be a (ground) program. For any set ✠ of default negations, let ✝ ✙ ✳ ✠ ✵ ✞ ✑ ❅ ❇ ❈ ✦ ✆ ☛ ✄ ✠ ✢ ✂ ✦ ✤ , where ✂ is the standard propositional derivation relation with each default negation ❅ ❇ ❈ ✂ being treated as a named atom ❅ ❇ ❈ ✂ . A partial stable model ☞ of ☛ is defined by a maximal fixpoint ✠ of the function that applies ✝ ✙ twice, ✝ ✰ ✙ ✳ ✠ ✵ ✞ ✠ , while satisfying ✠ ✎ ✝ ✙ ✳ ✠ ✵ , in the following way: for any atom ✄ , ✓ ✄ ✗ ☞ if ❅ ❇ ❈ ✄ ✗ ✠ , ✄ ✗ ☞ if ☛ ✄ ✠ ✂ ✄ , and ✄ is undefined otherwise. Notationally, any ✄ such that ✄ ✢ ✗ ☞ and ✓ ✄ ✢ ✗ ☞ represents that ✄ is undefined in ☞ . An answer set ✆ (also called a stable model) can then be defined as a special case by a fixpoint ✝ such that ✝ ✙ ✳ ✝ ✵ ✞ ✝ and ✆ ✞ ✑ ✄ ✆ ☛ ✄ ✝ ✂ ✄ ✤ .

Theorem 4.1 Let ☛ be a finite program, ✟ a set of propositions, and ✒ ✓ ✕ ✚ ✗ ✙ ✚ ✟ ✚ ✑ ✛ the goal rewrite system w.r.t. ☛ and ✟ .

Soundness: For any literal ▲ and any rewrite sequence

where each ❊ ✂ is either an abducible literal or a0 , if ✺ ✶ ✄ ☞ ☞ ☞ ✄ ✺ ✍ is consistent, then there exists a partial stable model ☞ of ☛ ✄ ✑ ❊ ✶ ✚ ✭ ✭ ✭ ✚ ❊ ✍ ✤ ✠ such that ▲ ✗ ✒ ✶ ✓ ✕ ✓ ✍ ✺ ✂ ✎ ☞ .

Completeness: For any set of atoms ✠ ✎ ✟ , and any literal ▲ in a partial stable model ☞ of ☛ ✄ ✠ , there exists a rewrite sequence

We say that a program ☛ has no odd loops if there is no odd loop starting with any literals (programs that have no odd loops are also called call-consistent [Dung, 1992]). It is wellknown that if ☛ has no odd loops, then the partial stable models of ☛ and the answer sets of ☛ coincide. We now show that for any goal, the underlying rewrite system will generate an approximation of a cover for any program ☛ , and exactly a cover when ☛ has no odd loops.

Theorem 4.2 Let ✒ ✓ ✕ ✚ ✗ ✙ ✚ ✟ ✚ ✑ ✛ be a goal rewrite system. Suppose ✁ is a proposition and

is a rewrite sequence such that each ❊ ✂ ✕ is either a0 or an abducible literal, and ✺ ✂ ✶ ✄ ☞ ☞ ☞ ✄ ✺ ✂ ✍ ✜ is consistent for each ■ . Then, if ☛ has no odd loops then

is a cover of ✁ . In general, for arbitrary ☛ we have

where ✯ is any cover of ✁ .

Consider again the boat example in Section 1. The Clark completion of ✸ ✦ ✰ ✺ ✼ ✾ ❀ ❀ is:

Since ★ ✾ ✦ ❃ , ❊ ❋ ✦ ❍ and ❖ ✦ ❀ ◗ ❘ ✸ ❍ ❋ ❃ are abducibles, so rewriting for ✸ ✦ ✰ ✺ ✼ ✾ ❀ ❀ terminates in one step, and produces the following cover:

Notice that the second explanation is not minimal. To get minimal ones, we have to compute prime implicants of the disjunction of explanations in the cover, which are ★ ✾ ✦ ❃ ✌ ✓ ❊ ❋ ✦ ❍ and ★ ✾ ✦ ❃ ✌ ❖ ✦ ❀ ◗ ❘ ✸ ❍ ❋ ❃ .

5 Related work

Traditionally, logic programming proof procedures have been defined abstractly in terms of derivation and refutation. Termination has been considered a separate, implementation issue. On the one hand, this separation is possible since the underlying semantics allows the completeness to be stated without resorting to termination. But completeness is rarely guaranteed in an implementation. On the other hand, the separation is also necessary since these procedures deal with nonground programs for which the problem of loop-checking is undecidable (even for function-free programs [Bol et al., 1991]). For answer set programming, however, loop handling has become a semantic issue: a sound and complete procedure cannot be defined without it. Thus, a distinct feature of our work is a mechanism of loop handling both for termination and for the implementation of the underlying semantics.

Completed programs have been used in query answering in abstract, abductive procedures in [Console et al., 1991; Denecker and Schreye, 1998; Fung and Kowalski, 1997] for non-ground programs with constraints. These procedures are defined for the three-valued completion semantics under the certainty mode of reasoning - computing bindings for which an (existential) goal is true in all indentedmodels. In our case the reasoning mode is brave - establishing whether a query is true in one of the intended models.

Our work is closely related to another abstract procedure, the Eshghi-Kowalski procedure (EKP) [Eshghi and Kowalski, 1989], which is sound and complete for ground programs under finite-failure three-valued stable models [Giordano et al., 1996]. Besides loop handling and termination, to some extent, one can say that our goal rewriting system (GRS) simulates EKP in a nontrivial way.

1. GRS incurs no backtracking! Backtracking is simulated by rewriting disjunctions, e.g., ✝ ✟ ✎ ✑ ✎ .
2. Loops that go through negation are handled in EKP by nested structures while in GRS by a flat structure using rewrite chains.

These features plus loop handling made it possible to formalize our system as a rewriting system benefiting from the known properties of term rewriting in the literature. This also distinguishes our use of rewrite systems from that by [Fung and Kowalski, 1997]. It seems remarkable that a form of nonmonotonic reasoning is just rewriting, two areas of research that had little connection previously.

To illustrate these feature, consider the following program

✼ ✌ ✭ ▲ ✫ ❅ ❇ ❈ ✦ ✼ a0 ✭ ★ ✫ ✦ ✼ ✱ ✭ ✦ ✫ ❅ ❇ ❈ ★ ❅ ❇ ❈ ✸ ✼ ✂ ✭ ✸ ✫ ✦

and the questionwhetherwe can prove ▲ . Wemay answer this question by the following reasoning: To have ▲ we must have ❅ ❇ ❈ ✦ (r1); To have ❅ ❇ ❈ ✦ wemust have either ★ or ✸ (r2) which requires having ✦ (r3 and r4). This results in a contradiction. Note that in this reasoning we need to remember what was required previously ( ❅ ❇ ❈ ✦ in this case). This is exactly how the proof is done by GRS

However, EKP will go through six nested levels, and do it twice through backtracking, before the same conclusion can be reached.

Rewriting can be applied to function-free programs for proving ground goals. The idea is that if every derived goal is ground, then all the mechanisms given in this paper apply directly. Obviously, if for every rule in the given program a variable that appears in the body also appears in the head, then a ground goal will be rewritten to another ground goal. Domain restricted programs [Niemel¨a, 1999] can be instantiated only on domain predicates over variables that do not appear in the head so that the resulting non-ground programs also satisfy this requirement. For example, the program given in the next section is domain restricted.

6 Applications and experimental results

We have implemented the writing framework in SWI-Prolog. In the following, we discuss the performance of our implementation on one particular application of abduction in logic programming, which is the problem of computing successor state axioms from a causal action theory [Lin, 2000].

Consider a logistics domain in which we have a truck and a package. We know that the truck and the package 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 is the package. Suppose that we have the following propositions: ta ✳ ☎ ✵ - the truck is at location ☎ initially; pa ✳ ☎ ✵ - the package is at location ☎ initially; in - the package is in the truck initially; ta ✳ ☎ ✚ ✞ ✚ ✠ ✵ - the truck is at location ☎ after the action of moving it from ✞ to ✠ is performed; pa ✳ ☎ ✚ ✞ ✚ ✠ ✵ - the package is at location ☎ after the action of moving the truck from ✞ to ✠ is performed; and in ✳ ✞ ✚ ✠ ✵ - the package is in the truck after the action of moving the truck from ✞ to ✠ is performed. We then have the following logic program:

The first rule is the effect axiom. The second rule is a causal rule which says that if a package is in the truck, then the package should be where the truck is. The rest are frame axioms. For instance, the third one is the frame axiom about ta, with the help of a new predicate taol: if the truck is initially at ☞ , and if one cannot prove that it will be elsewhere after the action is performed, then it should still be at ☞ .

As one can see, the above program, when fully instantiated over any given finite set ✎ of locations, has no odd loops. So our rewrite system will generate a cover for any query. Note that in the programwe have omitted domain predicate ❊ ✾ ✸ ✳ ✌ ✵ for each variable ✌ in the body of a rule (all the variables in the program refer to locations). Thus, the program is domain restricted and needs only to be instantiated for the variable ✌ in the fourth and sixth rules over the domain of locations.

Now let the set ✟ of abducibles be the following set:

The following table shows some of the results for ✎ ✞ ✑ ✌ ✚ ✱ ✚ a0 ✚ ✂ ✤ : 2

For instance, the row on pa✳ ✌ ✚ ✱ ✚ a0 ✵ says that for it to be true, the package must initially be at ✌ and cannot be inside the truck (otherwise, it would be moved along with the truck), and the computation took 0.1 seconds.The row on pa ✳ a0 ✚ ✱ ✚ a0 ✵ says that for it to be true, either the package was initially at a0 or it was inside the truck. The outputs for larger ✎ s are similar. The performance varies for different queries. For simple queries like ta ✳ ✌ ✚ ✱ ✚ a0 ✵ , their covers can be computed almost in constant time. The hardest one is for pa✳ a0 ✚ ✱ ✚ a0 ✵ which took 25 minutes when ✆ ✎ ✆ ✞ a0 .

2 On a PIII 1GHz PC with 512MB RAM running SWI-Prolog 3.2.9.

It is interesting to compare our system with an alternative for computing the cover of a query. As we mentioned in Section 2, the set of abductive explanations according to Kakas and Mancarella is actually a cover. One way of computing these abductive explanations is to add, for each proposition ✕ ✗ ✟ , the following two clauses ([Satoh and Iwayama, 1991]): ✕ ✫ ❅ ❇ ❈ ✓ ✕ and ✓ ✕ ✫ ❅ ❇ ❈ ✕ into the original program, and use the fact that there will be a one to one correspondence between abductive explanations of ✁ under the original program and answer sets of the new program that contain ✁ . So one can use an answer set generator, for example smodel or dlv, to compute a cover of query by generating all the answer sets in the new program that contain the query. However, the problem here is that there are too many such answer sets in this case. For instance, suppose there are ✰ locations, then the number of answer sets that contain any particular query is in the order of ✱ ✰ ✲ , roughly one half of the number of complete hypotheses, even for a very simple query like ta ✳ ✌ ✚ ✱ ✚ a0 ✵ . We do not know at the moment if there is any efficient way of using an answer set generator to compute a cover set of a query.

7 Future work

There are several directions for extending this work. One of them is to consider rewriting for non-ground logic programs for some restricted yet decidable classes of non-ground goals. Another important one is to extend this to programs with constraints of the form:

Our new definition of abduction can be extended to include these constraints straightforwardly. The challenge is in extending our rewriting system accordingly.

8 Acknowledgements

We would like to thank Ilkka Niemel¨a for helpful discussions related to the topics of this paper, and Ken Satoh for comments on earlier version of this paper. The first author's work was supported in part by the Research Grants Council of Hong Kong under Competitive Earmarked Research Grant HKUST6145/98E. The work by the second author was carried out mainly during his visits to Hong Kong University of Science and Technology and the Institute of Information Science, Academia Sinica in Taiwan.