that G has an object not in τ (A) and τ (F**), the pseudo-successor state axiom**
for G in Succτ (A) must be of the form succ(G) ≡ init(G) ∧ **Φ. Therefore from**
M1 |= ¬init(G) we get M1 |= ¬succ(α). Since α is any disjunct of φ**, we have**
proved that M1 |= ¬succ(φ). Therefore M1 |= succ(τ (F)). Thus M2 |= **succ**(F).

✷

## 7. Related Work

In planning, the most closely related work is the causal reasoning module in Wilkins's SIPE system (Wilkins, 1988). Wilkins writes (page 85, Wilkins, 1988): "Use of the STRIPS
assumptions has made operators unacceptably difficult to describe in previous classical planners... One of the primary reasons for this is that all effects of an action must be explicitly stated... Deductive causal theories are one of the **most important mechanisms used** by SIPE to alleviate problems in operator representation caused by the STRIPS assumption." This is certainly one of the motivations for our system as well. In SIPE, domain rules have triggers, preconditions, conditions, and effects. Informally, when the triggers become true in the new situation, SIPE would then check in sequence to see if the preconditions were true in the old situation, and the conditions are true in **the new situation. If all these** conditions are true, it will then deduce the effects. For instance, a SIPE causal rule for on(x, y**) in the blocks world would look like:** Causal-rule: Not-on Arguments: x, y, z; Trigger: on(x,y); Precondition: on(x,z);
Effects: not on(x,z);
In comparison, our domain rules are much simpler. For instance, our corresponding rule for the above SIPE rule is simply: Causes(on(x, y) ∧ y 6= z, on(x, z**)). We do not need**
procedural directives like triggers. To a large degree, we can see our system as a rational reconstruction of the causal reasoning module in SIPE. As we **have shown in Theorem 1,** the procedure used by our system is sound under a translation **to causal theories in the** situation calculus. While Wilkins also gave a translation of his causal rules to formulas in the situation calculus, he did not specify an underlying logic to reason about such formulas.

In fact, as shown by Lin (1995), such translations would not work.

For those familiar with PDDL, the original version by McDermott and the AIPS-98 Planning Competition Committee allows domain axioms over stratified theories. According to the manual of PDDL 1.2 (McDermott, 1998), "axioms are logical formulas that assert relationships among propositions that hold within a situation." The format for writing axioms in PDDL is as follows:

## (:Axiom

:vars (?x ?y ...) :context W
:implies P)