This article is cited in
1 paper
Complexity of quantifier elimination in the theory of ordinary differentially closed fields
D. Yu. Grigor'ev
Abstract:
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)<d_1$;
$\mathrm{deg}_{T_1,\dots,T_\varepsilon}(\varphi)$, $\mathrm{deg}_{T_1,\dots,T_\varepsilon}(f_i)<d_2$
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.
UDC:
518.5