An effective algorithm for quantifier elimination over algebraically closed fields using straight line programs Original Research Article

In this paper we obtain an effective algorithm for quantifier elimination over algebraically closed fields: For every effective infinite integral domain k, closed under the extraction of pth roots when the characteristic p of k is positive, and every prenex formula theta with r blocks of quantifiers involving s polynomials F1, h., Fs ε k[X1, h.,Xn] encoded in dense form, there exists a well-parallelizable algorithm without divisions whose output is a quantifier-free formula equivalent to theta. The sequential complexity of this algorithm is bounded by O(¦theta¦) + D(O(n))r, where ¦theta¦ is the length of theta and D ≥ n is an upper bound for 1 + bEi = 1s deg Fi, and the polynomials in the output are encoded by means of a straight line program. The complexity bound obtained is better than the bounds of the known elimination algorithms, which are of the type ¦theta¦.Dncr, where c ≥ 2 is a constant. This becomes notorious when r = 1 (i.e., when there is only one block of quantifiers): the complexity bounds known up to now are not less than Dn2, while our bound is DO(n). Moreover, in the particular case that there is only one block of existential quantifiers and the input polynomials are given by a straight line program, we construct an elimination algorithm with even better bounds which depend on the length of this straight line program: Given a formula of the type imagethere existsXn−m+…,there existsXn:F1(X1,…,Xn=0 logical and … logical and Fs(X1,…,Xn)image=0 logical andG1(X1,…,Xn)≠0 logical and … logical and Gs′(X1,…,Xn)≠0, where F1,h., Fs ε k[X1,h., Xn] are polynomials whose degrees in the m variables X − m + 1,h., Xn are bounded by an integer d ≥ m and G1,h.,Gs′ ε k[X1,h., Xn] are polynomials whose degrees in the same variables are bounded by an integer δ, this algorithm eliminates quantifiers in time L2.(s.s′.δ)O(1).dO(m), where L is the length of the straight line program that encodes F1,h., Fs, G1,h., Gs′.