A New Approach to Quantifier Elimination for Real Algebra

Abstract

Quantifier elimination for the elementary formal theory of real numbers is a fascinating area of research at the intersection of various field of mathematics and computer science, such as mathematical logic, commutative algebra and algebraic geometry, computer algebra, computational geometry and complexity theory. Originally the method of quantifier elimination was invented (among others by Th. Skolem) in mathematical logic as a technical tool for solving the decision problem for a formalized mathematical theory. For the elementary formal theory of real numbers (or more accurately of real closed fields) such a quantifier elimination procedure was established in the 1930s by A. Tarski, using an extension of Sturm’s theorem of the 1830s for counting the number of real zeros of a univariate polynomial in a given interval. Since then an abundance of new decision and quantifier elimination methods for this theory with variations and optimizations has been published with the aim both of establishing the theoretical complexity of the problem and of finding methods that are of practical importance (see Arnon 1988a and the discussion and references in Renegar 1992a, 1992b, 1992c for a comparison of these methods). For sub-problems such as elimination of quantifiers with respect to variables, that are linearly or quadratically restricted, specialized methods have been developed with good success (see Weispfenning 1988; Loos and Weispfenning 1993; Hong 1992d; Weispfenning 1997).