George E. Collins
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.
- Brown, W. S., On Eculid's Algorithm and the Computation of Polynomial Greatest Common Divisors,
J. ACM , vol. 18, no. 4 (Oct. 1971), pp. 478--504. Google Scholar
Digital Library
- Brown, W. S., and Traub, J. F., On Euclid's Algorithm and the Theory of Subresultants,
J. ACM , vol. 18, no. 4 (Oct. 1971), pp. 505--514. Google ScholarDigital Library - Cohen, P. J., Decision Procedures for Real and p-adic Fields,
Comm. Pure and Applied Math. , vol. XXII, no. 2 (March 1969), pp. 131--151.Google ScholarCross Ref
- Collins, G. E., Subresultants and Reduced Polynomial Remainder Sequences,
J. ACM , vol. 14, no. 1 (Jan. 1967), pp. 128--142. Google ScholarDigital Library - Collins, G. E., The Calculation of Multi-variate Polynomial Resultants,
J. ACM , vol. 18, no. 4 (Oct. 1971), pp. 515--532. Google ScholarDigital Library - Collins, G. E., Computer Algebra of Polynomials and Rational Functions,
Am. Math. Monthly , vol. 80, no. 7 (Aug.-Sept. 1973), pp. 725--755.Google Scholar - Collins, G. E., Efficient Quantifier Elimination for Elementary Algebra (abstract), Symposium on Complexity of Sequential and Parallel Numerical Algorithms, Carnegie-Mellon University, May 1973.Google Scholar
- Collins, G. E., Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition, to appear.Google Scholar
- Fischer, M. J., and Rabin, M. O., Super-Exponential Complexity of Presburger Arithmetic, M.I.T. MAC Tech. Memo. 43, Feb. 1974. Google ScholarDigital Library
- Goldhaber, J. K., and Ehrlich, G.,
Algebra , MacMillan Co., 1970.Google Scholar - Heindel, L. E., Integer Arithmetic Algorithms for Polynomial Real Zero Determination,
J. ACM , vol. 18, no. 4 (Oct. 1971), pp. 533--548. Google ScholarDigital Library - Loos, R. G. K., and Collins, G. E., Resultant Algorithms for Exact Arithmetic on Algebraic Numbers, to appear in
SIAM J. on Comp. Google Scholar - Marden, M.,
The Geometry of the Zeros of a Polynomial in a Complex Variable , Am. Math. Soc., Providence, 1949.Google Scholar - Musser, D. R., Algorithms for Polynomial Factorization (Ph.D. Thesis), Univ. of Wisconsin Computer Sciences Dept. Tech. Report No. 134, Sept. 1971. Google ScholarDigital Library
- Musser, D. R., Multivariate Polynomial Factorization, to appear in
J. ACM. Google Scholar - Rubald, C. M., Algorithms for Polynomials over a Real Algebraic Numer Field (Ph.D. Thesis), Computer Sciences Dept. Tech. Report No. 206, Jan. 1974. Google ScholarDigital Library
- Seidenberg, A., A New Decision Method for Elementary Algebra,
Annals of Math. , vol. 60, no. 2 (Sept. 1954), pp. 365--374.Google ScholarCross Ref - Tarski, A.,
A Decision Method for Elementary Algebra and Geometry , second ed., rev., Univ. of California Press, Berkeley, 1951.Google Scholar - van der Waerden, B. L.,
Modern Algebra , vol. I, F. Ungar Co., New York, 1953.Google Scholar
Index Terms
- Quantifier elimination for real closed fields by cylindrical algebraic decomposition--preliminary report
Recommendations
The complexity of quantifier elimination and cylindrical algebraic decomposition
ISSAC '07: Proceedings of the 2007 international symposium on Symbolic and algebraic computationThis paper has two parts. In the first part we give a simple and constructive proof that quantifier elimination in real algebra is doubly exponential, even when there is only one free variable and all polynomials in the quantified input are linear. The ...
A formal quantifier elimination for algebraically closed fields
AISC'10/MKM'10/Calculemus'10: Proceedings of the 10th ASIC and 9th MKM international conference, and 17th Calculemus conference on Intelligent computer mathematicsWe prove formally that the first order theory of algebraically closed fields enjoys quantifier elimination, and hence is decidable. This proof is organized in two modular parts. We first reify the first order theory of rings and prove that quantifier ...
Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra System
We propose a decision procedure for algebraically closed fields based on a quantifier elimination method. The procedure is intended to build proofs for systems of polynomial equations and inequations. We describe how this procedure can be carried out in ...
Comments