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.

Contenu

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 Cylindrical Algebraic 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.- Sturm-Habicht 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 Macaulay Determinant.- 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.