as a theory consisting of literals only. Alternatively, we could consider all atoms mentioned in P S; post  A S; *post* as "unsafe" after the application of the operator and delete the literals P S; post A S; *post*)) from the state specification, but consider the resulting state specification still as "legal" if P S; *post* is consistent. Since there does not seem to exist a standard model for the execution of conditional effects in the presence of partial state specifications, we adopt the first alternative as one arbitrary choice. It should be noted, however, that this decision influences some of the results we present below.

Similarly to the rule that A S; post 6 P S; *post* leads to an illegal state specification, we require that if the precondition is not satisfied by all states in Mod S or if the state specification is already inconsistent, the result of applying o to S results in . This leads to the definition of the function R, which defines the outcome of applying an operator o from the set of operators O to a state specification:

$$R\;\;S,o$$

$$ R$$
R 2
# $\bf2^{\Sigma}\times O\:\to\:2^{\Sigma}$ $\bf\left\{\begin{array}{l}S-\quad\;A\;\;S,post\;o\quad\quad\;\;A\;\;S,post\;o\end{array}\right.$  . 

$$\begin{array}{l l l}{{\mathrm{if~}S\;\;/\;\;}}&{{\mathrm{and}}}\\ {{S\;\;}}&{{p e\;\;o\;\;\;\mathrm{and}}}\\ {{A\;\;S,p o s t\;\;o\;\;\;\;\;/\;\;}}&{{\mathrm{and}}}\\ {{A\;\;S,p o s t\;\;o\;\;\;\;\;\;\;P\;\;S,p o s t\;\;o}}\end{array}$$

otherwise Example 2 Using the propositional atoms and operators from Example 1, we assume the following two state specifications S1 tex; ind *, and* S2 tex; ind; bbl; blg *. If we try to apply the* operator latex to S1, we notice that this results in *because*

A S1; post latex)) aux; idx; dvi; log; dvi ind ok ; P S1; post latex)) A S1; post latex)) dvi cite ok; dvi cite ok ; i.e., we have A S1; post latex)) 6 P S1; post latex)): On the other hand, we can apply bibtex successfully to S1: R S1; bibtex S2:
It is easily verified that the syntactic operation on a state specification using the function R
corresponds to state transitions on the states described by the specification. Proposition 1 Let S be a state specification, o be an operator, and o *be the induced state-transition* function. If R S; o 6j *, then*

$$M o d\ \ R\ \ S,o\ \ \ \ \ \ \ \ s\ \ \ s\ \ \ \ \ \theta_{o}\ \ s\ ,\ s\ \ \ \ \ S\ .$$
If R S; o , then either
$$I.\;\;M o d\;\;S\;\;\;\;\;\;\;\emptyset,\,o r$$
2. _there are two states_ $s_{1},\,s_{2}\quad\mbox{Mod}\;\;S\;\;\mbox{such that}\;A\;\;s_{1},\mbox{post}\;o\;\;\;/\;A\;\;s_{2},\mbox{post}\;o\;\;\;,$ _or_
3. there exists a state s Mod S such that o s *is undefined.*