Сложность разрешения теории первого порядка вещественно замкнутых полей

Обозначим через $\mathbb{Q}_m=\mathbb{Q}(\delta_1,\dots,\delta_m)$ упорядоченное поле, где $\delta_{i+1}$ является бесконечно малым относительно элементов поля $\mathbb{Q}_i$, $0\leqslant i<m$ (положим $\mathbb{Q}_0=\mathbb{Q}$). Пусть дана формула теории первого порядка вещественного замыкания поля $\mathbb{Q}_m$ следующего вида: $\exists X_{1,1}\dots\exists X_{1,s_1}\forall X_{2,1}\dots\forall X_{2,s_2}\dots\exists X_{a,1}\dots \exists X_{a,s_a}(P)$, где $P$ — бескванторная формула, содержащая $k$ атомарных подформул вида $(f_j\geqslant0)$, где многочлены $f_j\in\mathbb{Q}_m[X_{1,1},\dots,X_{1,s_1},\dots,X_{a,1},\dots,X_{a,s_a}]$ удовлетворяют следующим оценкам: $\mathrm{deg}_{\delta_1,\dots,\delta_m}(f_j)<d_0$, $\mathrm{deg}_{X_{1,1},\dots,X_{1,s_1},\dots,X_{a,1},\dots,X_{a,s_a}}(f_j)<d$ и абсолютная величина всякого целого числа, входящего в коэффициенты многочленов $f_j$, не превосходит $2^M$. Обозначим $n=s_1+\dots+s_a$ — число переменных и $a\leqslant n$ — число перемен кванторов в формуле. Построен алгоритм, который проверяет истинность формул указанного вида за время полиномиальное от $M$, $(kd)^{O(n)^{5a-2(m+1)}}$, $d_0^{m+n}$. Известные ранее алгоритмы для этой задачи имели сложность порядка $M(kd\,d_0^m)^{2O(n)}$. Библ. – 19 назв.