Quantifier Elimination and Cylindrical Algebraic Decomposition

Quantifier Elimination and Cylindrical Algebraic Decomposition edited by Bob F. Caviness, Jeremy R. Johnson.

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 st...

Full description

Saved in:
Bibliographic Details
Corporate Author: SpringerLink (Online service)
Other Authors: Caviness, Bob F. (Editor), Johnson, Jeremy R. (Editor)
Format: eBook
Language:English
Published: Vienna : Springer Vienna : Imprint: Springer, 1998.
Edition:1st ed. 1998.
Series:Texts & Monographs in Symbolic Computation, A Series of the Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria,
Springer eBook Collection.
Subjects:
Computer science—Mathematics.
Mathematical logic.
Algebraic geometry.
Algorithms.
Electronic resources (E-books)
Online Access:Click to view e-book
Holy Cross Note:Loaded electronically.
Electronic access restricted to members of the Holy Cross Community.
Table of Contents:
  • 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.

Similar Items