Complexity of deciding Tarski algebra (Q1264143)

Let (*) \(\exists x_{1,1}...\exists x_{1,s_ 1}\forall x_{2,1}...\forall x_{2,s_ 2}...\exists x_{a,1}...\exists x_{a,s_ a}(P)\) be a formula of Tarski algebra, where P is a quantifier-free formula with atomic subformulas \((f_ i\geq 0)\), \(f_ i\in {\mathbb{Z}}[X_{1,1},...,X_{a,s_ a}]\), \(n=s_ 1+...+s_ a\), degrees \(\deg (f_ i)\leq d\), and the absolute value of each integer coefficient of \(f_ i\) is supposed to be less than \(2^ M\), \(1\leq i\leq k\). The main purpose of the present paper is to prove the following theorem: One can design a decision algorithm for Tarski algebra which determines the truth value of a formula of the kind (*) within a time polynomial in \(M(kd)^{O(n)^{4a-2}}\).