Complexity of deciding the first-order theory of real closed fields

Let denote an ordered field, where _i+1 is infinitesimal relative to the elements of the field _i 0 i < m (by definition, ₀=). Given a formula of the first-order theory of the real closed field _m, of the following form:, where P is a quantifier-free formula containing k atomic subformulas of the form (f_j 0), where are polynomials such that, and the absolute value of any integer occurring in the coefficients of the polynomials f_j is at most 2_M. Let =S₁+...+S_a denote the number of variables anda n the number of quantifiers in the formula. An algorithm is constructed which decides the truth of formulas of the above form in polynomial time with respect to M,. Previously known algorithms for this problem had complexity of the order of.Translated from Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V. A. Steklova Akad. Nauk SSSR, Vol. 174, pp. 53–100, 1988.