Quantifier elimination for real closed fields by cylindrical algebraic decompostion

1. Brown, W.S., On Euclid's Algorithm and the Computation of Polynomial Greatest Common Divisors, J. ACM, vol. 18, no. 4 (Oct. 1971) pp. 478–504.

   Article  MathSciNet  Google Scholar 

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

   Article  MathSciNet  Google Scholar 

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

   Article  MathSciNet  Google Scholar 

4. Collins, G.E., Subresultants and Reduced Polynomial Remainder Sequences, J. ACM, vol. 14, no. 1, (Jan. 1967), pp. 128–142.

   Article  MathSciNet  Google Scholar 

5. Collins, G.E., The Calculation of Multivariate Polynomial Resultants, J. ACM, vol. 18, no. 4 (Oct. 1971), pp. 515–532.

   Article  MathSciNet  Google Scholar 

6. Collins, G.E., Computer Algebra of Polynomials and Rational Functions, Am. Math. Monthly, vol. 80, no. 7 (Aug.-Sept. 1973), pp. 725–755.

   Article  MathSciNet  Google Scholar 

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

8. Collins, G.E., Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition — Preliminary Report, Proceedings of EUROSAM 74, STGSAM Bulletin, Vol. 8, no. 3 (August 1974), pp. 80–90.

   Article  Google Scholar 

9. Fischer, M.J., and Rabin, M.O., Super-Exponential Complexity of Presburger Arithmetic, M.I.T. MAC Tech. Memo. 43, Feb. 1974.

   Google Scholar 

10. Goldhaber, J.K., and Ehrlich, G., Algebra, MacMillan Co., 1970.

    Google Scholar 

11. Heindel, L.E., Integer Arithmetic Algorithms for Polynomial Real Zero Determination, J. ACM, vo. 18, no. 4 (Oct. 1971), pp. 533–548.

    Article  MathSciNet  Google Scholar 

12. Loos, R., G.K., A Constructive Approach to Algebraic Numbers, SIAM Journal on Computing, to appear.

    Google Scholar 

13. Marden, M., The Geometry of the Zeros of a Polynomial in a Complex Variable, Am. Math. Soc., Providence, 1949.

    Google Scholar 

14. Musser, D.R., Algorithms for Polynomial Factorization (Ph.D. Thesis), Univ. of Wisconsin Computer Sciences Dept. Tech. Report No. 134, Sept. 1971.

    Google Scholar 

15. Musser, D.R., Multivariate Polynomial Factorization, J.ACM., Vol. 22, No. 2 (April 1975), pp. 291–308.

    Article  MathSciNet  Google Scholar 

16. Rubald, C.M., Algorithms for Polynomials over a Real Algebraic Number Field (Ph.D. Thesis), Computer Sciences Dept. Tech. Report No. 206, Jan. 1974.

    Google Scholar 

17. Seidenberg, A., A New Decision Method for Elementary Algebra, Annals of Math., vol. 60, no. 2 (Sept. 1954), pp. 365–374.

    Article  MathSciNet  Google Scholar 

18. Tarski, A., A Decision Method for Elementary Algebra and Geometry, second ed., rev., Univ. of California Press, Berkeley, 1951.

    MATH  Google Scholar 

19. van der Waerden, B.L., Modern Algebra, vol. I, F. Ungar Co., New York, 1953.

    Google Scholar 

20. Böge, W., private communication, June 1973

    Google Scholar 

21. Holthusen, C., Vereinfachungen für Tarski's Entscheidungsverfahren der Elementaren Reelen Algebra (Diplomarbeit, University of Heidelberg), January 1974.

    Google Scholar 

22. Collins, G.E., and E. Horowitz, The Minimum Root Separation of a Polynomial, Math. of Comp., Vol. 28, No. 126, (April 1974), pp. 589–597.

    Article  MathSciNet  Google Scholar 

23. Mignotte, M., An Inequality About Factors of Polynomials, Math. of Comp., Vol. 28, No. 128 (October 1974), pp. 1153–1157.

    Article  MathSciNet  Google Scholar 

24. Knuth, D.E., The Art of Computer Programming, Vol. 2: Seminumerical Algorithms, Addison-Wesley, Reading, 1969.

    MATH  Google Scholar 

25. Schönhage, A., and V. Strassen, Schnelle Multiplikation großer Zahlen, Computing, Vol. 7, pp. 281–292.

    Google Scholar 

26. Ferrante, J., and C. Rackoff, A Decision Procedure for the First Order Theory of Real Addition with Order, SIAM Journal on Computing, Vol. 4, No. 1 (March 1975), pp. 69–76.

    Article  MathSciNet  Google Scholar 

Download references