Quantifier Elimination

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

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.