\begin{thebibliography}{HCJE93} \bibitem[Arn81]{Arnon:81} D.S. Arnon. \newblock {\em Algorithms for the geometry of semi-algebraic sets}. \newblock Ph.d. dissertation, Computer Sciences Department, University of Wisconsin, Madison, 1981. \newblock Technical Report No. 436. \bibitem[CH91]{CollinsHong:91} George~E. Collins and Hoon Hong. \newblock Partial cylindrical algebraic decomposition for quantifier elimination. \newblock {\em Journal of Symbolic Computation}, 12(3):299--328, September 1991. \bibitem[Col75]{Collins:75} George~Edwin Collins. \newblock Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. \newblock In H.~Brakhage, editor, {\em Automata Theory and Formal Languages. 2nd GI Conference}, volume~33 of {\em Lecture Notes in Computer Science}, pages 134--183, Berlin, Heidelberg, New York, May 1975. Gesellschaft f\"ur Informatik, Springer-Verlag. \bibitem[DH88]{Davenport:88} James~H. Davenport and Joos Heintz. \newblock Real {Q}uantifier {E}limination is {D}oubly exponential. \newblock {\em Journal of Symbolic Computation}, 5(1\&2):29--35, February 1988. \bibitem[DS95a]{DolzmannSturm:95a} Andreas Dolzmann and Thomas Sturm. \newblock {\em Redlog, a Reduce Logic Package}. \newblock FMI, Universit\"at Passau, D-94030 Passau, Germany, preliminary edition, July 1995. \newblock User Manual. \bibitem[DS95b]{DolzmannSturm:95} Andreas Dolzmann and Thomas Sturm. \newblock Simplification of quan\-ti\-fier-free formulas over ordered fields. \newblock Technical Report MIP-9517, FMI, Universit\"at Passau, D-94030 Passau, Germany, October 1995. \newblock To appear in the Journal of Symbolic Computation. \bibitem[DS96]{DolzmannSturm:96} Andreas Dolzmann and Thomas Sturm. \newblock Redlog---computer algebra meets computer logic. \newblock Technical Report MIP-9603, FMI, Universit\"at Passau, D-94030 Passau, Germany, February 1996. \bibitem[DSW96]{DSW:96} Andreas Dolzmann, Thomas Sturm, and Volker Weispfenning. \newblock A new approach for automatic theorem proving in real geometry. \newblock Technical Report MIP-9611, FMI, Universit\"at Passau, D-94030 Passau, Germany, May 1996. \bibitem[HCJE93]{Hong:93} Hoon Hong, George~E. Collins, Jeremy~R. Johnson, and Mark~J. Encarnacion. \newblock {QEPCAD} interactive version 12. \newblock Kindly communicated to us by Hoon Hong, September 1993. \bibitem[Hen95]{Henning:91} Eckhard Henning. \newblock {Rechnergest\"utzte Dimensionierung analoger Schaltungen auf der Basis symbolischer Analyseverfahren}. \newblock Technical report, {Zentrum f\"ur Mikroelektronik}, December 1995. \newblock Jahresbericht zum Forschungsprojekt. \bibitem[Laz88]{Lazard:88} Daniel Lazard. \newblock Quantifier elimination: Optimal solution for two classical examples. \newblock {\em Journal of Symbolic Computation}, 5(1\&2):261--266, February 1988. \bibitem[LW93]{LoosWeispfenning:93} R\"udiger Loos and Volker Weispfenning. \newblock Applying linear quantifier elimination. \newblock {\em The Computer Journal}, 36(5):450--462, 1993. \newblock Special issue on computational quantifier elimination. \bibitem[NT92]{NoroTakeshima:92} M.~Noro and T.~Takeshima. \newblock {R}isa/{A}sir---a computer algebra system. \newblock In {\em Proceedings of the ISSAC '92}, pages 387--396, 1992. \bibitem[Tar48]{Tarski:48} A.~Tarski. \newblock A decision method for elementary algebra and geometry. \newblock Technical report, University of California, 1948. \newblock Second edn., rev. 1951. \bibitem[Wei88]{Weispfenning:88} Volker Weispfenning. \newblock The complexity of linear problems in fields. \newblock {\em Journal of Symbolic Computation}, 5(1):3--27, February 1988. \bibitem[Wei94a]{Weispfenning:95b} Volker Weispfenning. \newblock Parametric linear and quadratic optimization by elimination. \newblock Technical Report MIP-9404, FMI, Universit\"at Passau, D-94030 Passau, Germany, April 1994. \newblock To appear in the Journal of Symbolic Computation. \bibitem[Wei94b]{Weispfenning:94} Volker Weispfenning. \newblock Quantifier elimination for real algebra---the cubic case. \newblock In {\em Proceedings of the International Symposium on Symbolic and Algebraic Computation in Oxford}, pages 258--263, New York, July 1994. ACM Press. \bibitem[Wei96a]{Weispfenning:96b} Volker Weispfenning. \newblock Applying quantifier elimination to problems in simulation and optimization. \newblock Technical Report MIP-9607, FMI, Universit\"at Passau, D-94030 Passau, Germany, April 1996. \newblock To appear in the Journal of Symbolic Computation. \bibitem[Wei96b]{Weispfenning:96} Volker Weispfenning. \newblock Quantifier elimination for real algebra---the quadratic case and beyond. \newblock To appear in AAECC, 1996. \end{thebibliography}