**ACM84a**-
D. S. Arnon, George E. Collins, and Scott McCallum.

Cylindrical algebraic decomposition i: The basic algorithm.*SIAM Journal on Computing*, 13(4):865-877, 1984. **ACM84b**-
D. S. Arnon, George E. Collins, and Scott McCallum.

Cylindrical algebraic decomposition ii: An adjacency algorithm for the plane.*SIAM Journal on Computing*, 13(4):878-889, 1984. **AM88**-
D. S. Arnon and M. Mignotte.

On mechanical quantifier elimination for elementary algebra and geometry.*Journal of Symbolic Computation*, 5(1,2):237-260, 1988. **Arn88**-
D. S. Arnon.

A cluster-based cylindrical algebraic decomposition algorithm.*Journal of Symbolic Computation*, 5(1,2):189-212, 1988. **BC96**-
Christopher W. Brown and George. E. Collins.

Simple truth invariant CAD's and solution formula construction.

Technical Report 96-19, Research Institute for Symbolic Computation (RISC-Linz), 1996. **Bro**-
Christopher W. Brown.

Simple cad construction and its applications.

Accepted for publication in the Journal of Symbolic Computation. **Bro98**-
Christopher W. Brown.

Simplification of truth-invariant cylindrical algebraic decompositions.

In*Proc. International Symposium on Symbolic and Algebraic Computation*, pages 295-301, 1998. **Bro99a**-
Christopher W. Brown.

Guaranteed solution formula construction.

In*Proc. International Symposium on Symbolic and Algebraic Computation*, pages 137-144, 1999. **Bro99b**-
Christopher W. Brown.

Solution formula construction for truth invariant cad's.

Technical Report 99-07, University of Delaware, 1999. **Bro00**-
Christopher W. Brown.

Improved projection for cad's of .

In*Proc. International Symposium on Symbolic and Algebraic Computation*, 2000.

to appear. **Bro99**-
Christopher W. Brown.
*Solution Formula Construction for Truth Invariant CAD's*.

PhD thesis, University of Delaware, 99. **CH91**-
G. E. Collins and H. Hong.

Partial cylindrical algebraic decomposition for quantifier elimination.*Journal of Symbolic Computation*, 12(3):299-328, Sep 1991. **CJ98**-
B.F. Caviness and Jeremy R. Johnson, editors.
*Quantifier Elimination and Cylindrical Algebraic Decomposition*.

Texts and Monographs in Symbolic Computation. Springer-Verlag, 1998. **Coh69**-
P. J. Cohen.

Decision procedures for real and*p*-adic fields.*Comm. Pure and Applied Math.*, 22(2):131-151, March 1969. **Col73**-
George E. Collins.

Efficient quantifier elimination for elementary algebra.

Abstract presented at Symposium on Complexity of Sequential and Parallel Algorithms, Carnegie-Mellon University, May 1973. **Col74**-
G. E. Collins.

Quantifier elimination for real closed fields by cylindrical algebraic decomposition--preliminary report.

8(3):80-90, August 1974.

Proceedings of EUROSAM 74. **Col75**-
G. E. Collins.

Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition.

In*Lecture Notes In Computer Science*, volume Vol. 33, pages 134-183. Springer-Verlag, Berlin, 1975.

Reprinted in [CJ98]. **Col98**-
G. E. Collins.

Quantifier elimination by cylindrical algebraic decomposition - 20 years of progress.

In B. Caviness and J. Johnson, editors,*Quantifier Elimination and Cylindrical Algebraic Decomposition*, Texts and Monographs in Symbolic Computation. Springer-Verlag, 1998. **DH97**-
J. H. Davenport and Joos Heintz.

Real quantifier elimination is doubly exponential.*Journal of Symbolic Computation*, 5:29-35, 1997. **DS96**-
Andreas Dolzmann and Thomas Sturm.

Redlog - computer algebra meets computer logic.

Technical Report MIP-9603, FMI, Universität Passau, 1996. **DS97**-
Andreas Dolzmann and Thomas Sturm.

Simplification of quantifier-free formulae over ordered fields.*Journal of Symbolic Computation*, 24(2):209-231, Aug. 1997.

Special Issue on Applications of Quantifier Elimination. **FR74**-
M. J. Fischer and M. O. Rabin.

Super-exponential complexity of Pressburger arithmetic.*Complexity of Computation (AMS-SIAM Proceedings)*, 7:27-41, 1974. **GJ79**-
Michael R. Garey and David S. Johnson.
*Computers and Intractability - A Guide to the Theory of NP-Completeness*.

W. H. Freeman and Company, 1979. **Gri88**-
D. Yu. Grigor'ev.

The complexity of deciding tarski algebra.*Journal of Symbolic Computation*, 5:65-108, 1988. **HLS97**-
H. Hong, R. Liska, and S. Steinberg.

Testing stability by quantifier elimination.*Journal of Symbolic Computation*, 24(2):161-187, Aug. 1997.

Special Issue on Applications of Quantifier Elimination. **Hon90a**-
H. Hong.

An improvement of the projection operator in cylindrical algebraic decomposition.

In*Proc. International Symposium on Symbolic and Algebraic Computation*, pages 261-264, 1990. **Hon90b**-
H. Hong.
*Improvements in CAD-based Quantifier Elimination*.

PhD thesis, The Ohio State University, 1990. **Hon91**-
H. Hong.

Comparison of several decision algorithms for the existential theory of the reals.

Technical Report 91-41, Research Institute for Symbolic Computation (RISC-Linz), 1991. **Hon92**-
H. Hong.

Simple solution formula construction in cylindrical algebraic decomposition based quantifier elimination.

In*Proc. International Symposium on Symbolic and Algebraic Computation*, pages 177-188, 1992. **Hon93**-
H. Hong.

Quantifier elimination for formulas constrained by quadratic equations via slope resultants.*Computer J.*, 36(5):440-449, 1993. **HRS90**-
J. Heintz, M. Roy, and P. Solernó.

Sur la complexité du principe de Tarski-Seidenberg.*Bull. Soc. Math. France*, 118:101-126, 1990. **Jef97**-
D.J. Jeffrey.

Formulae, algorithms, and quartic extrema.*Mathematics Magazine*, 70:349 - 356, 1997. **Kah75**-
W. Kahan.

Problem no. 9: An ellipse problem.*SIGSAM Bulletin of the Assoc. Comp. Mach.*, 9(35):11, 1975. **Knu98**-
Donald E. Knuth.
*The Art of Computer Programming*, volume 3.

Addison-Wesley, second edition, 1998. **Laz88**-
D. Lazard.

Quantifier elimination: Optimal solution for two classical examples.*Journal of Symbolic Computation*, 5(1,2), 1988. **Laz90**-
D. Lazard.

An improved projection for cylindrical algebraic decomposition.

Unpublished manuscript, 1990. **McC56**-
E. J. McCluskey.

Minimization of boolean functions.*Bell Syst. Techn. J.*, 35:1417-1444, 1956. **McC84**-
S. McCallum.
*An Improved Projection Operator for Cylindrical Algebraic Decomposition*.

PhD thesis, University of Wisconsin-Madison, 1984. **McC88**-
S. McCallum.

An improved projection operation for cylindrical algebraic decomposition of three-dimensional space.*Journal of Symbolic Computation*, 1988. **McC93**-
S. McCallum.

Solving polynomial strict inequalities using cylindrical algebraic decomposition.*The Computer Journal*, 1993. **McC98a**-
S. McCallum.

An improved projection operator for cylindrical algebraic decomposition.

In B. Caviness and J. Johnson, editors,*Quantifier Elimination and Cylindrical Algebraic Decomposition*, Texts and Monographs in Symbolic Computation. Springer-Verlag, Vienna, 1998. **McC98b**-
S. McCallum.

A note about projection in the presence of an equational constraint.

Technical Report 99-01, University of Delaware, 1998. **McC99**-
S. McCallum.

On projection in cad-based quantifier elimination with equational constraint.

In Sam Dooley, editor,*Proc. International Symposium on Symbolic and Algebraic Computation*, pages 145-149, 1999. **Mis93**-
B. Mishra.
*Algorithmic Algebra*.

Springer-Verlag New York, Inc., 1993. **PRS93**-
P. Pedersen, M. Roy, and A. Szpirglas.

Counting real zeros in the multivariate case.

In F. Esyette and A. Galligo, editors,*Proc. MEGA'92*. Birkhäuser Boston, 1993. **Pug92**-
W. Pugh.

The omega test: a fast and practical integer programming algorithm for dependence analysis.*Communications of the ACM*, 8:102 - 114, 1992. **Qui55**-
W. V. O. Quine.

A way to simplify truth functions.*American Mathematical Monthly*, 62:626-631, 1955. **Qui79**-
J. R. Quinlan.

Discovering rules from large collections of examples: a case study.

In D. Michie, editor,*Expert Systems in the Microelectronic Age*. Edinburgh University Press, Edinburgh, 1979. **Ren92**-
J. Renegar.

On the computational complexity and geometry of the first-order theory of the reals, parts I-III.*Journal of Symbolic Computation*, 13:255-352, 1992. **Sei54**-
A. Seidenberg.

A new decision method for elementary algebra.*Annals of Math.*, 60(2):365-374, 1954. **SS81**-
J. Schwartz and M. Sharir.

On the `piano movers' problem. i. the case of a two-dimensional rigid polygonal body moving amidst polygonal barriers.

Technical Report 39, Department of Computer Science, Courant Institute of Mathematical Sciences, 1981. **Str94**-
A. Strzebonski.

An algorithm for systems of strong polynomial inequalities.*The Mathematica Journal*, 1994. **Str00**-
A. Strzebonski.

Solving systems of strict polynomial inequalities.*Journal of Symbolic Computation*, 29:471-480, 2000. **SW49**-
C. E. Shannon and W. Weaver.
*The Mathematical Theory of Communication*.

University of Illinois Press, Urbana, 1949. **SW97**-
T. Sturm and W. Weispfenning.

Rounding and blending of solids by a real elimination method.

In*Proc. IMACS World Congress*, pages 727-732, 1997. **Tar51**-
A. Tarski.
*A Decision Method for Elementary Algebra and Geometry*.

University of California Press, Berkeley, 1951.

second ed., rev. Reprinted in [CJ98]. **Wei88**-
V. Weispfenning.

The complexity of linear problems in fields.*Journal of Symbolic Computation*, 5:3-27, 1988. **Wei94**-
V. Weispfenning.

Quantifier elimination for real algebra -- the cubic case.

In*Proc. International Symposium on Symbolic and Algebraic Computation*, pages 258-263, 1994. **Wei97**-
V. Weispfenning.

Quantifier elimination for real algebra -- the quadratic case and beyond.*AAECC*, 8:85-101, 1997. **Wei98**-
V. Weispfenning.

A new approach to quantifier elimination for real algebra.

In B. Caviness and J. Johnson, editors,*Quantifier Elimination and Cylindrical Algebraic Decomposition*, Texts and Monographs in Symbolic Computation. Springer-Verlag, Vienna, 1998.

This document was generated using the
**LaTeX**2`HTML` translator Version 98.1p1 release (March 2nd, 1998)

Copyright © 1993, 1994, 1995, 1996, 1997, Nikos Drakos, Computer Based Learning Unit, University of Leeds.

The command line arguments were:

**latex2html** `-split 0 -no_navigation genbib.tex`.

The translation was initiated by Christopher W. Brown on 2000-07-27