Kooperativer Bibliotheksverbund

UID:

Umfang: XIX, 431 p. 16 illus. , online resource.

Ausgabe: 1st ed. 1998.

ISBN: 9783709194591

Serie: Texts & Monographs in Symbolic Computation, A Series of the Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria,

Inhalt: 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.

Anmerkung: 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.

In: Springer Nature eBook

Weitere Ausg.: Printed edition: ISBN 9783211827949

Weitere Ausg.: Printed edition: ISBN 9783709194607

Sprache: Englisch

DOI: 10.1007/978-3-7091-9459-1

URL: https://doi.org/10.1007/978-3-7091-9459-1