Quantifier elimination for real closed fields by cylindrical algebraic decomposition--preliminary report
- 1 August 1974
- journal article
- Published by Association for Computing Machinery (ACM) in ACM SIGSAM Bulletin
- Vol. 8 (3) , 80-90
- https://doi.org/10.1145/1086837.1086852
Abstract
Tarski in 1948, [18] published a quantifier elimination method for the elementary theory of real closed fields (which he had discovered in 1930). As noted by Tarski, any quantifier elimination method for this theory also provides a decision method, which enables one to decide whether any sentence of the theory is true or false. Since many important and difficult mathematical problems can be expressed in this theory, any computationally feasible quantifier elimination algorithm would be of utmost significance.Keywords
This publication has 8 references indexed in Scilit:
- Integer Arithmetic Algorithms for Polynomial Real Zero DeterminationJournal of the ACM, 1971
- The Calculation of Multivariate Polynomial ResultantsJournal of the ACM, 1971
- On Euclid's Algorithm and the Computation of Polynomial Greatest Common DivisorsJournal of the ACM, 1971
- On Euclid's Algorithm and the Theory of SubresultantsJournal of the ACM, 1971
- Decision procedures for real and p‐adic fieldsCommunications on Pure and Applied Mathematics, 1969
- Subresultants and Reduced Polynomial Remainder SequencesJournal of the ACM, 1967
- A New Decision Method for Elementary AlgebraAnnals of Mathematics, 1954
- A Decision Method for Elementary Algebra and GeometryPublished by University of California Press ,1951