عنوان

Quantifier elimination and cylindrical algebraic decomposition

(Number (ISBN

3709194598

(Number (ISBN

9783709194591

Number

b548044

Title Proper

Quantifier elimination and cylindrical algebraic decomposition

General Material Designation

[Book]

First Statement of Responsibility

B.F. Caviness, J.R. Johnson (eds.).

Place of Publication, Distribution, etc.

Wien ; New York

Name of Publisher, Distributor, etc.

Springer

Date of Publication, Distribution, etc.

©1998.

Specific Material Designation and Extent of Item

(xix, 431 pages) : illustrations

Series Title

Texts and monographs in symbolic computation.

Text of Note

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.

Text of Note

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.

Parallel Title

Quantifier elimination

Algebra -- Data processing -- Congresses.

Algorithms -- Congresses.

Decomposition method -- Data processing -- Congresses.

B.F. Caviness, J.R. Johnson (eds.).

Bob F Caviness

J R Johnson

Electronic name

[Book]

Y