New complexity bounds for cylindrical decompositions of sub-pfaffian sets
Savvas Pericleous, Nicolai Vorobjov · 2001
Tarski-Seidenberg principle plays a key role in many applications and algorithm of computer algebra. Moreover it is constructive, and some very efficient quantifier elimination algorithms appeared recently. However, Tarski-Seidenberg principle is wrong for first-order theories involving some real analytic functions (e.g. an exponential function). In this case a weaker statement is sometimes true, a possibility to eliminate one sort of quantifiers (either ∀ or ∃). We construct a new algorithm for a cylindrical cell decomposition of a closed cube In ⊄ Rn compatible with a semianalytic subset S ⊄ In, defined by Pfaffian functions. In particular the algorithm is able to eliminate one sort of quantifiers from a first-order formula. The complexity bound of the algorithm is doubly exponential in n2.