such that  o1;:::;on s is defined iff  o1;:::;oi s is defined for every i,  i  n. Using this notion, one can easily prove—using induction over the plan length—that any plan for an instance is **sound** in Lifschitz' (1986) sense, i.e., corresponds to the application of state transition functions to the initial states. Proposition 2 Let h ; I; Gi *be a planning instance and* ho1; : : : ; oni *be an element of* O?*. If* Res I; ) *is consistent, then*

$$s\quad s\quad\quad\theta_{\Delta}\;\;s\;,\;s\quad\quad\mathbf{I}\;\;.$$
$$M o d\;\;R e s\;\;{\bf I}\,,$$
Mod Res I; )) s s  s ; s I :
If Res I; ) *is inconsistent, then either* 1. Mod I ;*, or*

2. there exists a (possibly empty) prefix ho1; : : : ; oii (  i  n  ) of *such that* S
$\mathbf{1}_1\lor\sigma_1:\cdot\cdot\cdot$ . 
Res I; ho1 ; : : : ; oii and either
(a) there are two states s1; s2 Mod S *such that* A s1; *post* oi+1)) 6 A s2; *post* oi+1)),
or
(b) there exists a state s Mod S *such that* oi+1 s *is undefined.*

## 2.2 A Family Of Propositional Planning Formalisms

The propositional variant of standard STRIPS (Fikes & Nilsson, 1971), which we will also call S
in what follows, is a planning formalism that requires complete state specifications, *unconditional* effects, and *propositional atoms* as formulae in the precondition lists. Less restrictive planning formalisms can have the following additional features: Incomplete state specifications (I): The state specifications may not be complete. Conditional Effects (C): Effects can be conditional. Literals as formulae ( ): The formulae in preconditions and effect conditions can be literals.

Boolean formulae (B): The formulae in preconditions and effect conditions can be arbitrary boolean formulae.

These extensions can also be combined. We will use combinations of letters to refer to such multiple extensions. For instance, S refers to the formalism S extended by literals in the precondition lists, SIC refers to the formalism allowing for incomplete state specifications and conditional effects, and SBIC , finally, refers to the general planning formalism introduced in Section 2.1.

Example 4 When we consider the planning instance from Example 3, it becomes quickly obvious that this instance has been expressed using SLIC *. The initial state specification is* incomplete, the operator latex *contains* conditional effects *and negative* literals *in some effect conditions. However,* we do not need general Boolean formulae *to express the instance.*