New Complexity Bounds for Cylindrical Decompositions of Sub-Pfaffian Sets

Tarski-Seidenberg principle plays a key role in real algebraic geometry and its applications. It is also constructive and some efficient quantifier elimination algorithms appeared recently. However, the principle is wrong for first-order theories involving certain real analytic functions (e.g., an exponential function). In this case a weaker statement is sometimes true, a possibility to eliminate onesort ofq uantifiers (either ∀ or ∃). We construct an algorithm for a cylindrical cell decomposition ofa closed cube In ⊂ Rn compatible with a semianalytic subset S ⊂ In, defined by analytic functions from a certain broad finitely defined class (Pfaffian functions), modulo an oracle for deciding emptiness of such sets. In particular the algorithm is able to eliminate one sort ofq uantifiers from a first-order formula. The complexity of the algorithm and the bounds on the output are doubly exponential in O(n2).