Totality For reasoning under incomplete, but total knowledge K provides (f positive):
total f if B after A. ⇔caused f if not −f, B after A.

caused −f if not f, B after A.

This is is for instance useful to model non-deterministic action effects. For a discussion of the full impact of this statement in modeling planning under incomplete knowledge and non-determinism, we refer to our previous paper on the language K (Eiter et al., 2003b).

State Integrity For integrity constraints that refer to the preceding state, K provides forbidden B after A. ⇔ caused false if B after A.

Non-executability For specifying that some action is not executable, K provides nonexecutable a if B. ⇔ caused false after a, B.

By this definition, nonexecutable overrides executable in case of conflicts.

Sequential Plans To exclude simultaneous execution of actions, K provides noConcurrency. ⇔ caused false after a1, a2.

where a1 and a2 range over all possible actions such that a1, a2 ∈ LPD ∩ Lact and a1 6= a2.

In all macros, "if B" (resp. "after A") can be omitted, if B (resp. A) is empty.

## Appendix B. Proofs

Proof of Theorem 4.4: *Membership (i):* The problems are in NP resp. **NPMV**, since if l is polynomial in the size of P, any optimistic plan P = hA1**, . . . , A**li for P with a supporting trajectory T = ht1**, . . . , t**ii for P can be guessed and, by Proposition 4.1, verified in polynomial time. Furthermore, **cost**P(P) ≤ b can be efficiently checked, since **cost**P(P) is easily computed (all costs are constants).

Hardness (i): K is a fragment of Kc, and each K planning problem can be viewed as the problem of deciding the existence of resp. finding an admissible plan wrt. cost 0. As was previously shown
(Eiter et al., 2003b), deciding existence of an optimistic plan for a given K planning problem is NP-hard for fixed plan length l; hence, it is also NP-hard for Kc.

We show that finding an optimistic plan is hard for **NPMV** by a reduction from the well-known SAT problem, cf. (Papadimitriou, 1994), whose instances are CNFs φ = c1**∧· · ·∧**ck of clauses ci =
Li,1 ∨ · · · ∨Li,mi
, where each Li,j is a classical literal over propositional atoms X = {x1**, . . . , x**n}.

Consider the following planning domain PDφ for φ:
fluents : x1**. . . . x**n. state0. state1. actions : c1 costs 1**. . . . c**k costs 1.

ax1**. . . . ax**n.

initially : total x1**. . . .** total xn.

caused state0.

always : caused state1 after state0.

executable c1 after ¬.L1,1**, . . . ,** ¬.L1,m1

.

forbidden after ¬.L1,1**, . . . ,** ¬.L1,m1

, not c1.

· · ·
executable ck after ¬.Lk,1, . . . , ¬.Lk,mk

.

forbidden after ¬.Lk,1, . . . , ¬.Lk,mk

, not ck.

executable ax1 after x1. forbidden after x1, not ax1.

· · ·
executable axn after xn. forbidden after xn, not axn.