Complexity of quantifier elimination in the theory of ordinary differentially closed fields

D. Yu. Grigor'ev

Zapiski Nauchnykh Seminarov POMI, Computational complexity theory. Part 4, Tome 176 (1989), pp. 53-67

Résumé

Let a formula of the first-order theory of ordinary differentially closed fields $Q_1u_1\dots Q_nu_n(\Omega)$ be given, where $Q_1,\dots,Q_n$ are quantifiers and $\Omega$ is quantifier-free with atomic subformulas of the kind ($f_i=0$), $1\leqslant i\leqslant N$, here $f_i\in F\{u_1,\dots,u_n,v_1,\dots,v_n\}$ are differential polynomials (with respect to differentiation in $X$). The field $F\simeq\mathbb{Q}(T_1,\dots,T_\varepsilon)[Z]/(\varphi)$ where $T_1,\dots,T_\varepsilon$ are algebraically independent over $\mathbb{Q}$ and the polynomial $\varphi\in\mathbb{Q}(T_1,\dots,T_\varepsilon)[Z]$ is irreducible. Assume that the orders $\mathrm{ord}_{u_s}(f_i)\leqslant r$, $\mathrm{ord}_{v_t}(f_i)\leqslant r$ and the degree of $f_i$ considered as a polynomial in all the variables $X$, $u_1,u_1^{(1)},\dots,u_1^{(r)},\dots,u_n,u_n^{(1)},\dots,u_n^{(r)},v_1,v_1^{(1)},\dots,v_1^{(r)},\dots,v_m,v_1^{(1)},\dots,v_m^{(r)}$ is less than $d$, where $v_t^{(s)}=d^sv_t/dX^s$, moreover $\mathrm{deg}_Z(\varphi)$; $\mathrm{deg}_{T_1,\dots,T_\varepsilon}(\varphi)$, $\mathrm{deg}_{T_1,\dots,T_\varepsilon}(f_i)$ and the bit-size of each rational coefficient occurring in $\varphi$ and in $f_i$ is less than $M$. THEOREM. One can produce a quantifier-free formula equivalent in the theory of differentially closed fields to $Q_1u_1\dots Q_nu_n(\Omega)$ in time $(M(((Nd)^{m^n}d_1d_2)^{O(1)^{r2^n}})^{\varepsilon+m})^{O(1)}$. The previously known quantifier elimination procedure for this theory due to A. Seidenberg has a non-elementary complexity.