The paper is organi ed as follows.  n  ection   we discuss the results on the compu tational comple ity of conditional planning, which are the motivation for the approach we have chosen. ection presents di erent translations of conditional planning to uantified olean formulae.  The more general framework of conditional planning allows more degrees of freedom in choosing what kind of plans a planner produces.    e consider a general for mali ation in which internal state transitions of a plan are described as finite automata, and less general formali ations with more restricted transition functions. or all formali ations we present translations of problem instances to  uantified   oolean formulae.

untified olean formula that illustrates the translations is given in  ection  .    e have solved a nmber of simple problems in conditional planning by using a theorem prover for we have developed. The theorem prover is brie y discussed in  ection   and the e  periments in ection . inally, in ection we discuss earlier work that is related to ours.

## 2. Preliminaries

uantified oolean formulae are of the form 1 1 2 2 2 2 2 n n where is an un uantified propositional formula and the prefi  consists of universal V and e istential 3  uantifiers n and the propositional variables as the l formula that is obtained from    by replacing occurrences 1 of the propositional variable by the formula . The truth of  uantified   oolean formulae is defined recursively as follows.

The truth of a formula that does not contain variables, that is, that consists of the constants true and false and connectives, is defined in the obvious way by truth tables for the connectives.    formula ∃    is true if and only if or is true.   formula V
are true.    amples of true  uantified  oolean is true if and only if and formulae are ∀
and ∃ ∃ 
and A A
are false. hanging the order of two consecutive variables uantified by the same uantifier does not a  ect the truth value of the formula.  t is often useful to ignore the ordering of consecutive variables and view each   uantifier as   uantifying a set of formulae, for e  ample 3 1 2V 1 2D. The si e of a  uantified   oolean formula can be defined as the number of occurrences of propositional variables in it.

The interest in  uantified   oolean formulae in the theory of computational comple ity stems from the fact that like propositional satisfiability characteri es the problems in NP, uantified oolean formulae with di erent prefi es characteri e di erent classes in the polynomial hierarchy    alca ar et al., problems that are solvable in polynomial time by a deterministic Turing machine. NP is the class of decision problems that are solvable in polynomial time by a nondeterministic Turing maine.  The class co NP consists of those problems the complements of whi are in NP.  n general, the class co   consists of problems whose complements are in the class
. The polynomial hierarchy P   is an infinite hierarchy of comple ity classes 
, and 0 that is defined by using oracle Turing machines in the following way.

A for all

 $$\begin{array}{cccccccccccccc}&p&&&&&p&&&&&\Delta_0^p&=&&&&&\\ &0&&&&&p&&&&&0&&&&&\\ &p&&&&&p&&&&&p&&&&&\Delta_{i\,+\,1}^p&=&&&&&\Sigma_i^p\\ &&&\end{array}$$  **1.** We assume that `noseed` quantifiers do not quantify the same variable. 