Cylindrical algebraic decomposition i: The basic algorithm.
SIAM Journal on Computing, 13(4):865-877, 1984.
Cylindrical algebraic decomposition ii: An adjacency algorithm for the plane.
SIAM Journal on Computing, 13(4):878-889, 1984.
On mechanical quantifier elimination for elementary algebra and geometry.
Journal of Symbolic Computation, 5(1,2):237-260, 1988.
A cluster-based cylindrical algebraic decomposition algorithm.
Journal of Symbolic Computation, 5(1,2):189-212, 1988.
Simple truth invariant CAD's and solution formula construction.
Technical Report 96-19, Research Institute for Symbolic Computation (RISC-Linz), 1996.
Simple cad construction and its applications.
Accepted for publication in the Journal of Symbolic Computation.
Simplification of truth-invariant cylindrical algebraic decompositions.
In Proc. International Symposium on Symbolic and Algebraic Computation, pages 295-301, 1998.
Guaranteed solution formula construction.
In Proc. International Symposium on Symbolic and Algebraic Computation, pages 137-144, 1999.
Solution formula construction for truth invariant cad's.
Technical Report 99-07, University of Delaware, 1999.
Improved projection for cad's of
.
In Proc. International Symposium on Symbolic and Algebraic Computation, 2000.
to appear.
Solution Formula Construction for Truth Invariant CAD's.
PhD thesis, University of Delaware, 99.
Partial cylindrical algebraic decomposition for quantifier elimination.
Journal of Symbolic Computation, 12(3):299-328, Sep 1991.
Quantifier Elimination and Cylindrical Algebraic Decomposition.
Texts and Monographs in Symbolic Computation. Springer-Verlag, 1998.
Decision procedures for real and p-adic fields.
Comm. Pure and Applied Math., 22(2):131-151, March 1969.
Efficient quantifier elimination for elementary algebra.
Abstract presented at Symposium on Complexity of Sequential and Parallel Algorithms, Carnegie-Mellon University, May 1973.
Quantifier elimination for real closed fields by cylindrical algebraic decomposition--preliminary report.
8(3):80-90, August 1974.
Proceedings of EUROSAM 74.
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].
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.
Real quantifier elimination is doubly exponential.
Journal of Symbolic Computation, 5:29-35, 1997.
Redlog - computer algebra meets computer logic.
Technical Report MIP-9603, FMI, Universität Passau, 1996.
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.
Super-exponential complexity of Pressburger arithmetic.
Complexity of Computation (AMS-SIAM Proceedings), 7:27-41, 1974.
Computers and Intractability - A Guide to the Theory of NP-Completeness.
W. H. Freeman and Company, 1979.
The complexity of deciding tarski algebra.
Journal of Symbolic Computation, 5:65-108, 1988.
Testing stability by quantifier elimination.
Journal of Symbolic Computation, 24(2):161-187, Aug. 1997.
Special Issue on Applications of Quantifier Elimination.
An improvement of the projection operator in cylindrical algebraic decomposition.
In Proc. International Symposium on Symbolic and Algebraic Computation, pages 261-264, 1990.
Improvements in CAD-based Quantifier Elimination.
PhD thesis, The Ohio State University, 1990.
Comparison of several decision algorithms for the existential theory of the reals.
Technical Report 91-41, Research Institute for Symbolic Computation (RISC-Linz), 1991.
Simple solution formula construction in cylindrical algebraic decomposition based quantifier elimination.
In Proc. International Symposium on Symbolic and Algebraic Computation, pages 177-188, 1992.
Quantifier elimination for formulas constrained by quadratic equations via slope resultants.
Computer J., 36(5):440-449, 1993.
Sur la complexité du principe de Tarski-Seidenberg.
Bull. Soc. Math. France, 118:101-126, 1990.
Formulae, algorithms, and quartic extrema.
Mathematics Magazine, 70:349 - 356, 1997.
Problem no. 9: An ellipse problem.
SIGSAM Bulletin of the Assoc. Comp. Mach., 9(35):11, 1975.
The Art of Computer Programming, volume 3.
Addison-Wesley, second edition, 1998.
Quantifier elimination: Optimal solution for two classical examples.
Journal of Symbolic Computation, 5(1,2), 1988.
An improved projection for cylindrical algebraic decomposition.
Unpublished manuscript, 1990.
Minimization of boolean functions.
Bell Syst. Techn. J., 35:1417-1444, 1956.
An Improved Projection Operator for Cylindrical Algebraic Decomposition.
PhD thesis, University of Wisconsin-Madison, 1984.
An improved projection operation for cylindrical algebraic decomposition of three-dimensional space.
Journal of Symbolic Computation, 1988.
Solving polynomial strict inequalities using cylindrical algebraic decomposition.
The Computer Journal, 1993.
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.
A note about projection in the presence of an equational constraint.
Technical Report 99-01, University of Delaware, 1998.
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.
Algorithmic Algebra.
Springer-Verlag New York, Inc., 1993.
Counting real zeros in the multivariate case.
In F. Esyette and A. Galligo, editors, Proc. MEGA'92. Birkhäuser Boston, 1993.
The omega test: a fast and practical integer programming algorithm for dependence analysis.
Communications of the ACM, 8:102 - 114, 1992.
A way to simplify truth functions.
American Mathematical Monthly, 62:626-631, 1955.
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.
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.
A new decision method for elementary algebra.
Annals of Math., 60(2):365-374, 1954.
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.
An algorithm for systems of strong polynomial inequalities.
The Mathematica Journal, 1994.
Solving systems of strict polynomial inequalities.
Journal of Symbolic Computation, 29:471-480, 2000.
The Mathematical Theory of Communication.
University of Illinois Press, Urbana, 1949.
Rounding and blending of solids by a real elimination method.
In Proc. IMACS World Congress, pages 727-732, 1997.
A Decision Method for Elementary Algebra and Geometry.
University of California Press, Berkeley, 1951.
second ed., rev. Reprinted in [CJ98].
The complexity of linear problems in fields.
Journal of Symbolic Computation, 5:3-27, 1988.
Quantifier elimination for real algebra -- the cubic case.
In Proc. International Symposium on Symbolic and Algebraic Computation, pages 258-263, 1994.
Quantifier elimination for real algebra -- the quadratic case and beyond.
AAECC, 8:85-101, 1997.
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.