Quantifier Elimination and Cylindrical Algebraic Decomposition

1. Front Matter

   Pages i-xix

   PDF

2. Introduction

   • Bob F. Caviness, Jeremy R. Johnson

   Pages 1-7

3. Quantifier Elimination by Cylindrical Algebraic Decomposition — Twenty Years of Progress

   • George E. Collins

   Pages 8-23

4. A Decision Method for Elementary Algebra and Geometry

   • Alfred Tarski

   Pages 24-84

5. Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition

   • George E. Collins

   Pages 85-121

6. Super-Exponential Complexity of Presburger Arithmetic

   • Michael J. Fischer, Michael O. Rabin

   Pages 122-135

7. Cylindrical Algebraic Decomposition I: The Basic Algorithm

   • Dennis S. Arnon, George E. Collins, Scott McCallum

   Pages 136-151

8. Cylindrical Algebraic Decomposition II: An Adjacency Algorithm for the Plane

   • Dennis S. Arnon, George E. Collins, Scott McCallum

   Pages 152-165

9. An Improvement of the Projection Operator in Cylindrical Algebraic Decomposition

   • Hoon Hong

   Pages 166-173

10. Partial Cylindrical Algebraic Decomposition for Quantifier Elimination

    • George E. Collins, Hoon Hong

    Pages 174-200

11. Simple Solution Formula Construction in Cylindrical Algebraic Decomposition Based Quantifier Elimination

    • Hoon Hong

    Pages 201-219

12. Recent Progress on the Complexity of the Decision Problem for the Reals

    • James Renegar

    Pages 220-241

13. An Improved Projection Operation for Cylindrical Algebraic Decomposition

    • Scott McCallum

    Pages 242-268

14. Algorithms for Polynomial Real Root Isolation

    • J. R. Johnson

    Pages 269-299

15. Sturm—Habicht Sequences, Determinants and Real Roots of Univariate Polynomials

    • L. González-Vega, T. Recio, H. Lombardi, M.-F. Roy

    Pages 300-316

16. Characterizations of the Macaulay Matrix and Their Algorithmic Impact

    • Georg Hagel

    Pages 317-326

17. Computation of Variant Resultants

    • Hoon Hong, J. Rafael Sendra

    Pages 327-340

18. A New Algorithm to Find a Point in Every Cell Defined by a Family of Polynomials

    • Saugata Basu, Richard Pollack, Marie-Françoise Roy

    Pages 341-350

19. Local Theories and Cylindrical Decomposition

    • Daniel Richardson

    Pages 351-364

20. A Combinatorial Algorithm Solving Some Quantifier Elimination Problems

    • Laureano González-Vega

    Pages 365-375

George Collins’ discovery of Cylindrical Algebraic Decomposition (CAD) as a method for Quantifier Elimination (QE) for the elementary theory of real closed fields brought a major breakthrough in automating mathematics with recent important applications in high-tech areas (e.g. robot motion), also stimulating fundamental research in computer algebra over the past three decades. This volume is a state-of-the-art collection of important papers on CAD and QE and on the related area of algorithmic aspects of real geometry. It contains papers from a symposium held in Linz in 1993, reprints of seminal papers from the area including Tarski’s landmark paper as well as a survey outlining the developments in CAD based QE that have taken place in the last twenty years.

• Algebraic Computation
• Symbolic Computation
• Symbolisches Rechnen
• Variable
• algorithms
• calculus
• complexity
• geometry
• proof

"... The book is a nearly complete presentation of the history of the developement of CAD algorithms and its applications, and is suitable for the beginner as well as the expert ...” Zentralblatt für Mathematik

• Department of Computer and Information Sciences, University of Delaware, Newark, USA

  Bob F. Caviness

• Department of Mathematics and Computer Science, Drexel University, Philadelphia, USA

  Jeremy R. Johnson

Policies and ethics