Abstract:
Let a formula with $a$ quantifier alternations be given having atomic subformulas of the kind ($f_j\geqslant0$) with polynomials $f_i$ as in [5]. Deciding algorithm is designed with complexity $(M(kd)^{(O(n))^{5a-2(m+1)}}\cdot d_0^{(m+n)})^{O(1)}$.