×

Definability and fast quantifier elimination in algebraically closed fields. (English) Zbl 0546.03017

A celebrated theorem of Tarski asserts the existence of a primitively recursive procedure for elimination of quantifiers in algebraically closed fields. The present work - an extended version of papers by J. Heintz and R. Wüthrich [SIGSAM Bull. 9, No.4, 11 (1975)] and by J. Heintz [Fundamentals of computation theory ’79, Proc. Conf., Berlin/Wendisch-Rietz 1979, 160-166 (1979; Zbl 0439.03003)] - is devoted to the theorem above and to related definability problems from the point of view of complexity.
The main result proved in this paper shows that there exists a quantifier elimination procedure for algebraically closed fields with a time bound which is polynomial in degree and maximum length of the coefficients of the polynomials appearing in the input formula but double exponential in the number of variables of the input formula. A closely related question concerning the cardinality of the finite sets definable by prenex first order formulas in the language of fields is also investigated. The main parameters occurring in the answer to this question are the sum of the degrees of the polynomials, the total number of variables, and the number of bounded variables in the formulas under consideration. The method is based on a version of Bezout’s theorem without multiplicities, called by the author the Bezout-inequality.
Reviewer: S.A.Basarab

MSC:

03C10 Quantifier elimination, model completeness, and related topics
03D15 Complexity of computation (including implicit computational complexity)
12L99 Connections between field theory and logic
03C60 Model-theoretic algebra
13L05 Applications of logic to commutative algebra
14A25 Elementary questions in algebraic geometry

Citations:

Zbl 0439.03003
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Atiyah, M. F.; Macdonald, I. G., Introduction to Commutative Algebra (1969), Addison-Wesley: Addison-Wesley Reading, MA · Zbl 0175.03601
[2] Bareiss, E. H., Sylvester’s identity and multistep integer preserving Gaussian elimination, Math. Comput., 22, 103, 565-578 (1968) · Zbl 0187.09701
[3] Baur, W.; Strassen, V., The complexity of partial derivatives, Theoret. Comput. Sci., 22, 317-330 (1983) · Zbl 0498.68028
[4] Collins, G. E., Quantifier elimination for real closed fields by cylindrical algebraic decomposition, (Lecture Notes in Computer Science, 33 (1975), Springer: Springer Berlin), 134-183 · Zbl 0318.02051
[5] Edmonds, J., Systems of distinct representatives and linear algebra, J. Res. Nat. Bur. Standards, 71B, 4, 241-245 (1967) · Zbl 0178.03002
[6] Fischer, M. J.; Rabin, M. D., Super-exponential complexity of Presburger arithmetic, MAC Technical Memorandum 43 M.I.T. (1974) · Zbl 0319.68024
[7] J. Heintz, Definability bounds in algebraically closed fields and a note on degree in affine algebraic geometry, Presented at the 1977 Oberwolfach Conference on Complexity Theory.; J. Heintz, Definability bounds in algebraically closed fields and a note on degree in affine algebraic geometry, Presented at the 1977 Oberwolfach Conference on Complexity Theory.
[8] Heintz, J., Definability bounds of first order theories of algebraically closed fields, Ext. abstract, (Budach, L., Fundamentals of Computation Theory FCT ’79 (1979), Akademie-Verlag: Akademie-Verlag Berlin), 160-166 · Zbl 0439.03003
[9] Heintz, J.; Schnorr, C. P., Testing polynomials which are easy to compute, Proc. 12th Annual Symposium ACM on Computing. Proc. 12th Annual Symposium ACM on Computing, Logic and Algorithmic. An International Symposium Held in Honour of Ernst Specker. Proc. 12th Annual Symposium ACM on Computing. Proc. 12th Annual Symposium ACM on Computing, Logic and Algorithmic. An International Symposium Held in Honour of Ernst Specker, Monographie No. 30 de L’Enseignement Mathématique, 237-254 (1982), Geneva · Zbl 0483.68043
[10] Heintz, J.; Sieveking, M., Lower bounds for polynomials with algebraic coefficients, Theoret. Comput. Sci., 11, 321-330 (1980) · Zbl 0452.68051
[11] Heintz, J.; Sieveking, M., Absolute primality of polynomials is decidable in random polynomial time in the number of variables, (Proc. 8th Colloquium Automata, Languages and Programming. Proc. 8th Colloquium Automata, Languages and Programming, Lecture Notes in Computer Science, 115 (1981), Springer: Springer Berlin), 16-28 · Zbl 0462.68025
[12] Heintz, J.; Wüthrich, R., An efficient quantifier elimination algorithm for algebraically closed fields of any characteristic, SIGSAM Bull., 9, 4, 11 (1975)
[13] Hermann, G., Die Frage der endlich vielen Schritte in der Theorie der Polynomideale, Math. Ann., 95, 736-788 (1926)
[14] Iversen, B., Generic Local Structure of the Morphisms in Commutative Algebra, (Lecture Notes in Mathematics, 310 (1973), Springer: Springer Berlin) · Zbl 0247.13001
[15] Lang, S., Algebra (1969), Addison-Wesley: Addison-Wesley Reading, MA · Zbl 0176.00504
[16] Lang, S., Introduction to Algebraic Geometry (1972), Addison-Wesley: Addison-Wesley Reading, MA · Zbl 0247.14001
[17] Monck, L., An elementary-recursive decision procedure for \(Th(R\), +, ·) (1974), University of California: University of California Berkeley, Department of Mathematics
[18] D. Mumford, Introduction to Algebraic Geometry; D. Mumford, Introduction to Algebraic Geometry · Zbl 0114.13106
[19] Samuel, P., Méthodes d’Algèbre Abstraite en Géometrie Algébrique (1967), Springer: Springer Berlin · Zbl 0146.16901
[20] Schnorr, C. P., An extension of Strassen’s degree bound, SIAM J. Comput., 10, 371-382 (1981) · Zbl 0475.68017
[21] Seidenberg, A., Constructions in algebra, Trans. Amer. Math. Soc., 197, 273-313 (1974) · Zbl 0356.13007
[22] Shafarevich, I. R., Basic Algebraic Geometry (1974), Nauka: Nauka Moscow, in English: Springer, Berlin · Zbl 0284.14001
[23] Solovay, R., Private communication (1975)
[24] Strassen, V., Die Berechnungskomplexität von elementarsymmetrischen Funktionen und von Interpolationskoeffizienten, Numer. Math., 20, 238-251 (1973) · Zbl 0251.65036
[25] Strassen, V., The computational complexity of continued fractions, Proc. 1981 ACM Symposium on Symbolic and Algebraic Computation, 51-67 (1981) · Zbl 0486.68029
[26] van der Waerden, B. L., Algebra I, (8. Auflage der Modernen Algebra (1971), Springer: Springer Berlin), HT Bd. 12 · Zbl 0137.25403
[27] Wüthrich, H. R., Ein Entscheidungsverfahren für die Theorie der reellabgeschlossenen Körper, (Specker, E.; Strassen, V., Komplexität von Entcheidungsproblemen. Ein Seminar. Komplexität von Entcheidungsproblemen. Ein Seminar, Lecture Notes in Computer Science, 43 (1976), Springer: Springer Berlin), 138-162 · Zbl 0363.02052
[28] Wüthrich, H. R., Ein schnelles Quantoreneliminationsverfahren für die Theorie der algebraisch abgeschlossenen Körper, (Ph.D. Thesis (1977), University of Zurich) · Zbl 0363.02052
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.