New Results On Quantifier Elimination Over Real Closed Fields and Applications to Constraint Databases

In this paper we give a new algorithm for quantifier elimination in the first order theory of real closed fields that improves the complexity of the best known algorithm for this problem until now. Unlike previously known algorithms [3, 25, 20] the combinatorial part of the complexity of this new algorithm is independent of the number of free variables. Moreover, under the assumption that each polynomial in the input depend only on a constant number of free variable, the algebraic part of the complexity can also be made independent of the number of free variables. This new feature of our algorithm allows us to obtain a new algorithm for a variant of the quantifier elimination problem. We give an almost optimal algorithm for this new problem, which we call the Uniform Quantifier Elimination Problem. Using the uniform quantifier elimination algorithm, we give an algorithm for solving a problem arising in the field of constraint databases with real polynomial constraints. We give an algorithm for converting a query with natural domain semantics to an equivalent one with active domain semantics. A non-constructive version of this result was proved in [4]. Very recently, a constructive proof was also given independently in [6]. However, complexity issues were not considered and no algorithm with a reasonable complexity bound was know for this latter problem until now.
We also point out interesting logical consequences of this algorithmic result, concerning the expressive power of a constraint query language over the reals. This leads to simpler and constructive proofs for these inexpressibility results than the ones known before.
Moreover, our improved algorithm for performing quantifier elimination immediately leads to improved algorithms for several problems for which quantifier elimination is a basic step, for example, the problem of computing the closure of a given semi-algebraic set.