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).
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.
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].
