Quantifier Elimination and Cylindrical Algebraic Decomposition

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.

The book serves as an introduction and survey of the field of algorithmic quantifier elimination

Zusammenfassung
"... 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

Inhalt
1 Introduction to the Method.- 2 Importance of QE and CAD Algorithms.- 3 Alternative Approaches.- 4 Practical Issues.- Acknowledgments.- Quantifier Elimination by Cylindrical Algebraic Decomposition Twenty Years of Progress.- 1 Introduction.- 2 Original Method.- 3 Adjacency and Clustering.- 4 Improved Projection.- 5 Partial CADs.- 6 Interactive Implementation.- 7 Solution Formula Construction.- 8 Equational Constraints.- 9 Subalgorithms.- 10 Future Improvements.- A Decision Method for Elementary Algebra and Geometry.- 1 Introduction.- 2 The System of Elementary Algebra.- 3 Decision Method for Elementary Algebra.- 4 Extensions to Related Systems.- 5 Notes.- 6 Supplementary Notes.- Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition.- 1 Introduction.- 2 Algebraic Foundations.- 3 The Main Algorithm.- 4 Algorithm Analysis.- 5 Observations.- Super-Exponential Complexity of Presburger Arithmetic.- 1 Introduction and Main Theorems.- 2 Algorithms.- 3 Method for Complexity Proofs.- 4 Proof of Theorem 3 (Real Addition).- 5 Proof of Theorem 4 (Lengths of Proofs for Real Addition).- 6 Proof of Theorems 1 and 2 (Presburger Arithmetic).- 7 Other Results.- Cylindrical Algebraic Decomposition I: The Basic Algorithm.- 1 Introduction.- 2 Definition of Cylindrical Algebraic Decomposition.- 3 The Cylindrical Algebraic Decomposition Algorithm: Projection Phase.- 4 The Cylindrical Algebraic Decomposition Algorithm: Base Phase.- 5 The Cylindrical Algebraic Decomposition Algorithm: Extension Phase.- 6 An Example.- Cylindrical Algebraic Decomposition II: An Adjacency Algorithm for the Plane.- 1 Introduction.- 2 Adjacencies in Proper Cylindrical Algebraic Decompositions.- 3 Determination of Section-Section Adjacencies.- 4 Construction of Proper CylindricalAlgebraic Decompositions.- 5 An Example.- An Improvement of the Projection Operator in Cylindrical Algebraic Decomposition.- 1 Introduction.- 2 Idea.- 3 Analysis.- 4 Empirical Results.- Partial Cylindrical Algebraic Decomposition for Quantifier Elimination.- 1 Introduction.- 2 Main Idea.- 3 Partial CAD Construction Algorithm.- 4 Strategy for Cell Choice.- 5 Illustration..- 6 Empirical Results.- 7 Conclusion.- Simple Solution Formula Construction in Cylindrical Algebraic Decomposition Based Quantifier Elimination.- 1 Introduction.- 2 Problem Statement.- 3 (Complex) Solution Formula Construction.- 4 Simplification of Solution Formulas.- 5 Experiments.- Recent Progress on the Complexity of the Decision Problem for the Reals.- 1 Some Terminology.- 2 Some Complexity Highlights.- 3 Discussion of Ideas Behind the Algorithms.- An Improved Projection Operation for Cylindrical Algebraic Decomposition.- 1 Introduction..- 2 Background Material..- 3 Statements of Theorems about Improved Projection Map.- 4 Proof of Theorem 3 (and Lemmas).- 5 Proof of Theorem 4 (and Lemmas).- 6 CAD Construction Using Improved Projection.- 7 Examples.- 8 Appendix.- Algorithms for Polynomial Real Root Isolation.- 1 Introduction.- 2 Preliminary Mathematics.- 3 Algorithms.- 4 Computing Time Analysis.- 5 Empirical Computing Times.- SturmHabicht Sequences, Determinants and Real Roots of Univariate Polynomials.- 1 Introduction.- 2 Algebraic Properties of Sturm-Habicht Sequences.- 3 Sturm-Habicht Sequences and Real Roots of Polynomial.- 4 Sturm-Habicht Sequences and Hankel Forms.- 5 Applications and Examples.- Characterizations of the Macaulay Matrix and Their Algorithmic Impact.- 1 Introduction.- 2 Notation.- 3 Definitions of the Macaulay Matrix.- 4 Extraneous Factor and First Properties of the MacaulayDeterminant.- 5 Characterization of the Macaulay Matrix.- 6 Characterization of the Macaulay Matrix, if It Is Used to Calculate the u-Resultant.- 7 Two Sorts of Homogenization.- 8 Characterization of the Matrix of the Extraneous Factor.- 9 Conclusion.- Computation of Variant Resultants.- 1 Introduction.- 2 Problem Statement.- 3 Review of Determinant Based Method.- 4 Quotient Based Method.- 5 Modular Methods..- 6 Theoretical Computing Time Analysis.- 7 Experiments.- A New Algorithm to Find a Point in Every Cell Defined by a Family of Polynomials.- 1 Introduction.- 2 Proof of the Theorem.- Local Theories and Cylindrical Decomposition.- 1 Introduction.- 2 Infinitesimal Sectors at the Origin.- 3 Neighborhoods of Infinity.- 4 Exponential Polynomials in Two Variables.- A Combinatorial Algorithm Solving Some Quantifier Elimination Problems.- 1 Introduction.- 2 Sturm-Habicht Sequence.- 3 The Algorithms.- 4 Conclusions.- A New Approach to Quantifier Elimination for Real Algebra.- 1 Introduction.- 2 The Quantifier Elimination Problem for the Elementary Theory of the Reals.- 3 Counting Real Zeros Using Quadratic Forms.- 4 Comprehensive Gröbner Bases.- 5 Steps of the Quantifier Elimination Method.- 6 Examples.- References.