Effective algorithms for differentially closed fields

36 Views Asked by At

There are (many) model-theoretic proofs that $DCF_0$, the theory of differentially closed fields of characteristic zero admits quantifier elimination (see "Model Theory" by Marker, Chapter 4 or "A Course in Model Theory" by Ziegler and Tent, Chapter 3), but I can't find any effective algorithm that takes a formula $\phi$ (over the language of differential rings) and constructs an equivalent quantifier-free formula. Is such an algorithm even known? Alternatively, is there a known effective algorithm for deciding $DCF_0$ that possibly does not use full quantifier elimination?