THE COMPLEXITY OF THE DECISION PROBLEM FOR THE FIRST ORDER THEORY OF ALGEBRAICALLY CLOSED FIELDS
D. Yu. Grigor'ev · Mathematics of the USSR-Izvestiya · 1987
An algorithm is described that constructs, from every formula of the first order theory of algebraically closed fields, an equivalent quantifier-free formula in time which is polynomial in , where is the size of the formula, is the number of variables, and is the number of changes of quantifiers. Bibliography: 15 titles.