|
Zapiski Nauchnykh Seminarov LOMI, 1989, Volume 176, Pages 53–67
(Mi znsl4533)
|
|
|
|
This article is cited in 1 scientific paper (total 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.
Citation:
D. Yu. Grigor'ev, “Complexity of quantifier elimination in the theory of ordinary differentially closed fields”, Computational complexity theory. Part 4, Zap. Nauchn. Sem. LOMI, 176, "Nauka", Leningrad. Otdel., Leningrad, 1989, 53–67; J. Soviet Math., 59:3 (1992), 814–822
Linking options:
https://www.mathnet.ru/eng/znsl4533 https://www.mathnet.ru/eng/znsl/v176/p53
|
|