Quantifier elimination is a method of transforming a formula into an equivalent quantifier-free formula. Since quantifier-free formulae are easy to reason, quantifier elimination is useful for deduction and many quantifier-elimination procedures have been developed. Above all, quantifier-eliminationprocedures called "quantifier elimination by virtual substitutions" are known to be suitable for practical implementation. The idea of the virtual substitution based methods is to use a finit set of test cases, called an elimination set.
- B. F. Caviness, and J.R. Johnson (eds.), Quantifier Elimination and Cylindrical Algebraic Decomposition, Springer, Heidelberg, 1998.
- R. Loos and V. Weispfenning, Applying Linear Quantifier Elimination, Computer Journal, Vol.36, No. 5, pp450-462, 1993.
- How to obtain elimination sets
- A. Dolzmann and T. Sturm, Simplification of Quantifier-Free Formulae over Ordered Fields, Journal of Symbolic Computation, Vol. 24, No. 2, pp209-231, 1997.
- How to simplify quantifier-free formulae
