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).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag/Wien
About this paper
Cite this paper
Weispfenning, V. (1998). A New Approach to Quantifier Elimination for Real Algebra. In: Caviness, B.F., Johnson, J.R. (eds) Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation. Springer, Vienna. https://doi.org/10.1007/978-3-7091-9459-1_20
Download citation
DOI: https://doi.org/10.1007/978-3-7091-9459-1_20
Publisher Name: Springer, Vienna
Print ISBN: 978-3-211-82794-9
Online ISBN: 978-3-7091-9459-1
eBook Packages: Springer Book Archive