Other methods for solving the quantifier elimination problem have been
proposed since the introduction of the CAD based algorithm. The
methods of Renegar [Renegar(1992)] and of Heintz * et. al.*
[Heintz et al.(1990)Heintz, Roy, and Solernó] are both doubly exponential in the number
of quantifier alternations rather than the number of variables.
Renegar claimed that Grigor'ev's decision procedure
[Grigor'ev(1988)] could be extended to a quantifier elimination
algorithm, the complexity of which would be doubly exponential in the
number of quantifier alternations, though inferior to that of
Renegar and of Heintz * et. al.*.
In [Weispfenning(1998)], Weispfenning
introduced another approach to quantifier elimination, based on
comprehensive Gröbner bases and the work of Pedersen, Roy, and
Szpirglas [Pedersen et al.(1993)Pedersen, Roy, and
Szpirglas]. No asymptotic analysis was
given.

Other research has focused on the consideration of restrictions of the
full theory of real closed fields. For example, Weispfenning
[Weispfenning(1988)] considered formulas in which bound variables
appear only linearly. Hong [Hong(1993)] treated the case of an
input formula of the form

where is a quantifier free formula. Finally, Weispfenning [Weispfenning(1994),Weispfenning(1997)] has developed a method for attacking certain formulas in which the quantified variables appear at most cubically. The method has been implemented and has successfully dealt with many problems that would be impractical for the CAD-based method. Its complexity is not dependent on the number of free variables in , which is valuable in many problems. He also indicates how the method might be extended to the full theory, i.e. no degree restrictions.

The quantifier elimination problem is inherently doubly exponential in the number of variables [Fischer and Rabin(1974),Davenport and Heintz(1997)], so any algorithm for the full theory must work within these bounds. Despite this imposing worst case time complexity, there is hope that many non-trivial problems will be solvable in a reasonable amount of time. My goal is to improve the CAD algorithm to enlarge the scope of its practical applicability.