resulting state specification is legal when the application of all state-transformation functions leads to a theory that can be represented as a set of literals, it seems unlikely that there exists a scheme that preserves plan size polynomially. The reason for this pessimistic conjecture is that under this semantics it appears to be coNP-hard to determine whether the state specification resulting from applying a SLIC -operator is legal.

As a second step in showing that partial state specifications and literals can be compiled away, we show that we can compile SLC to S . The key idea in the proof is the same as in the proof of Theorem 6. We replace each negative literal p by a new atom pe. In order to detect inconsistencies introduced by conditional effects, we add to each postcondition conditional effects of the form p; pe ) . Further, to check that the last operator in a plan does not introduce any inconsistencies, we force the application of a "checking" operator that contains the same conditional effects. Lemma 8 SLC is polynomial-time compilable to S *preserving plan size exactly.* Proof. Let h ; I; Gi be a SLC -instance with h ; Oi. Since is a SLC -instance, the postconditions of all operators o O have the following form:
post o L1 ) K1; : : : ; Lm ) Km ;
with Lj ; Kj  .

As in the proof of Theorem 6, eshall be a disjoint copy of , and L is the set of atoms where each negative literal p is replaced by the atom pe. Now let *post* go be the following set

post go fLj ) Kj :Kj Lj ) Kj post o :
Further, let *cons* be the set of conditional effects

$$\begin{array}{r l}{c o n s}&{{}\quad p\,,{\tilde{p}}}\end{array}\Rightarrow$$
cons ffp; pe ) p ;
let g be an atom not appearing in , let oe be

$$\hat{\sigma}$$
oe hpre o ; post go *cons* f> ) ggi;
$$\mathrm{\boldmath~\left(\nabla\tilde{\bf~O}~\right.~}\quad\left.\tilde{o}\right.\right.\left.o\right.\left.\right.\left.\right.,\left.\mathrm{\boldmath~\left(\nabla\tilde{\bf~O}~\right.~}\right)$$

let Oeoe o O , and let the operator og be

$\downarrow$ . 
$\alpha$

$$\tau\;o_{g}\;\;\mathrm{be}$$
$$\begin{array}{c c c}{{o_{g}}}&{{}}&{{\left\langle\begin{array}{c}{{}}\\ {{}}\end{array},c o n s\right.}}\end{array}$$

og h>; *cons* f> ) ggi:
Then we can specify a compilation scheme f from SLC to S as follows:

tg (; G G:
f () h eg ; Oeoggi;
$$f_{\xi}$$
$$f_{i}$$
$$f_{g}$$
fi() f:g ;
$${\mathbf{}}J{\mathbf{}}{\mathbf{}}{\mathbf{}}{\mathbf{}}{\mathbf{}}$$
fg () g ;
$$\begin{array}{r l}{{}}&{{}^{\mathbf{o}\,\mathbf{x}}}\\ {{}}&{{}t_{i}\quad,\mathbf{I}}\\ {{}}&{{}t_{g}\quad,\mathbf{G}}\end{array}$$
ti(; I I :I;
The scheme f obviously satisfies conditions (2) and (3), all the functions can be computed in polynomial time, and F () is a S -instance.