Decision problem for a class of univariate Pfaffian functions (Q6122406)

Pfaffian functions, introduced by \textit{A. G. Khovanskij} [Sov. Math., Dokl. 22, 762--765 (1980; Zbl 0569.32004); translation from Dokl. Akad. Nauk SSSR 255, 804--807 (1980)], are a class of analytic functions that fulfil first-order partial differential equations with polynomial coefficients. To elaborate, consider a function \(\phi\) that satisfies the differential equation \(\phi'(x) = \Phi(x, \phi(x))\), where \(\Phi\) belongs to \(\mathbb{Z}[x,y]\) and has a positive degree in \(y\). Given any polynomial \(F\) in \(\mathbb{Z}[x,y]\), the expression \(F(x, \phi(x))\) is called a Pfaffian function associated with \(\phi\). Suppose \(\Phi\) represents a quantifier-free formula in \(x\), incorporating Pfaffian functions \(g_1, \ldots, g_s\). The main result of this paper is the existence of a symbolic method which determines the truth value of the statement \(\exists x\Psi\) in a real interval that falls within \(\phi\)'s domain. Additionally, this paper delves into the complexity associated with this procedure.