Quantifier Elimination (original) (raw)
Algebra Applied Mathematics Calculus and Analysis Discrete Mathematics Foundations of Mathematics Geometry History and Terminology Number Theory Probability and Statistics Recreational Mathematics Topology
Alphabetical Index New in MathWorld
Quantifier elimination is the removal of all quantifiers (the universal quantifier 
and existential quantifier 
) from a quantified system. A first-order theory allows quantifier elimination if, for each quantified formula, there exists an equivalent quantifier-free formula. Examples of such theories include the real numbers with
,
,
, and 
, and the theory of complex numbers with 
, 
, and 
. Quantifier elimination is implemented in as Resolve[_expr_].
Unfortunately, the worst-case time-complexity for real quantifier elimination is doubly exponential in the number of quantifier blocks (Weispfenning 1988, Davenport and Heintz 1988, Heintz et al. 1989, Caviness and Johnson 1998).
See also
Cylindrical Algebraic Decomposition, Existential Quantifier,Quantifier, Tarski's Theorem, Universal Quantifier
Explore with Wolfram|Alpha
References
Caviness, B. F. and Johnson, J. R. (Eds.). Quantifier Elimination and Cylindrical Algebraic Decomposition. New York:Springer-Verlag, 1998.Collins, G. E. "Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition." In Proc. 2nd GI Conf. Automata Theory and Formal Languages. New York:Springer-Verlag, pp. 134-183, 1975.Collins, G. E. "Quantifier Elimination by Cylindrical Algebraic Decomposition--Twenty Years of Progress." In Quantifier Elimination and Cylindrical Algebraic Decomposition (Ed. B. F. Caviness and J. R. Johnson). New York:Springer-Verlag, pp. 8-23, 1998.Collins, G. E. and Hong, H. "Partial Cylindrical Algebraic Decomposition for Quantifier Elimination." J. Symb. Comput. 12, 299-328, 1991.Davenport, J. H. "Computer Algebra for Cylindrical Algebraic Decomposition." Report TRITA-NA-8511, NADA, KTH, Stockholm, Sept. 1985.Davenport, J. and Heintz, J. "Real Quantifier Elimination Is Doubly Exponential."J. Symb. Comput. 5, 29-35, 1988.Dolzmann, A. and Sturm, T. "Simplification of Quantifier-Free Formulae over Ordered Fields." J. Symb. Comput. 24, 209-231, 1997.Dolzmann, A. and Weispfenning, V. "Local Quantifier Elimination." http://www.fmi.uni-passau.de/~dolzmann/refs/MIP-0003.ps.Z.Heintz, J.; Roy, R.-F.; and Solerno, P. "Complexité du principe de Tarski-Seidenberg."C. R. Acad. Sci. Paris Sér. I Math. 309, 825-830, 1989.Loos, R. and Weispfenning, V. "Applying Lattice Quantifier Elimination." Comput. J. 36, 450-461, 1993.Strzebonski, A. "Solving Algebraic Inequalities." Mathematica J. 7, 525-541, 2000.Weispfenning, V. "The Complexity of Linear Problems in Fields." J. Symb. Comput. 5, 3-27, 1988.
Referenced on Wolfram|Alpha
Cite this as:
Weisstein, Eric W. "Quantifier Elimination." From MathWorld--A Wolfram Web Resource. https://mathworld.wolfram.com/QuantifierElimination.html