Abstract
An algorithm is described producing for each formula of the first order theory of algebraically closed fields an equivalent free of quantifiers one. Denote by N a number of polynomials occuring in the formula, by d an upper bound on the degrees of polynomials, by n a number of variables, by a a number of quantifier alternations (in the prefix form). Then the algorithm works within the polynomial in the formula's size and in (Nd)n (2a+2) time. Up to now a bound (Nd)n o(n) was known ([5], [7], [15]).
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Chistov A.L., Grigor'ev D.Yu. Polynomial-time factoring of the multivariable polynomials over a global field. — LOMI preprint E-5-82, Leningrad, 1982.
Chistov A.L., Grigor'ev D.Yu. Subexponential-time solving systems of algebraic equations. I. — LOMI preprint E-9-83, Leningrad, 1983.
Chistov A.L., Grigor'ev D.Yu. Subexponential-time solving systems of algebraic equations. II. — LOMI preprint E-10-83, Leningrad, 1983.
Chistov A.L., Grigor'ev D.Yu. Polynomial-time factoring of polynomials and subexponential-time solving systems and quantifier elimination. — Notes of Scientific seminars of LOMI, Leningrad, 1984, vol. 137.
Collins G.E. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. — Lect.Notes Comput.Sci., 1975, vol.33, p. 134–183.
Grigor'ev D.Yu. Multiplicative complexity of a bilinear form over a commutative ring. — Lect.Notes Comp.Sci., 1981, vol.118, p.281–286.
Heintz J. Definability and fast quantifier elimination in algebraically closed fields. — Prepr.Univ.Frankfurt, West Germany, December, 1981.
Kaltofen E. A polynomial reduction from multivariate to bivariate integral polynomial factorization. — Proc. 14-th ACM Symp.Th. Comput., May, N.Y., 1982, p.261–266.
Kaltofen E. A polynomial-time reduction from bivariate to univariate integral polynomial factorization. — Proc.23-rd IEEE Symp.Found Comp.Sci., October, N.Y., 1982, p.57–64.
Lazard D. Algébre linéaire sur k[X 1,...,X n] et élimination. — Bull.Soc.Math.France, 1977, vol.105, p.165–190.
Lazard D. Résolutions des systèmes d'équations algébriques. — Theor Comput.Sci., 1981, vol.15, p.77–110.
Lenstra A.K., Lenstra H.W., Lovasz L. Factoring polynomials with rational coefficients. — Math.Ann., 1982, vol.261, p.515–534.
Lenstra A.K. Factoring multivariate polynomials over finite fields. — Preprint Math.Centrum Amsterdam, IW 221/83, Februari, 1983.
Shafarevich I.R. Basic algebraic geometry. — Springer-Verlag, 1974.
Wüthrich H.R. Ein Entscheidungsverfahren für die Theorie der reellabgeschlossenen Körper. — Lect.Notes Comput.Sci., 1976, vol.43, p.138–162.
Zariski O., Samuel P. Commutative algebra, vol.1, 2. — van Nostrand, 1960.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1984 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chistov, A.L., Grigor'ev, D.Y. (1984). Complexity of quantifier elimination in the theory of algebraically closed fields. In: Chytil, M.P., Koubek, V. (eds) Mathematical Foundations of Computer Science 1984. MFCS 1984. Lecture Notes in Computer Science, vol 176. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0030287
Download citation
DOI: https://doi.org/10.1007/BFb0030287
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-13372-8
Online ISBN: 978-3-540-38929-3
eBook Packages: Springer Book Archive