Symbolic techniques for the decidability of formulas involving E-polynomials over the reals

BARBAGALLO, MARÍA LAURA; JERONIMO, GABRIELA; SABIA, JUAN

Congreso; International Congress of Mathematicians; 2018

International Mathematical Union

In 1948, Tarski posed the decidability problem for the first order theory of the reals extended with exponentiation. This question was partly answered by Macintyre and Wilkie in 1996 under the assumption that Schanuel's conjecture in number theory is valid. More recently, the problem has been addressed from the algorithmic point of view for certain fragments of the theory; however, known algorithms mainly rely on numerical techniques and complexity issues have not been studied.We will present new symbolic algorithmic tools with a computable complexity to solve the decision problem for formulas involving E-polynomials. More precisely, given a non-constant univariate polynomial h with integer coefficients, we consider formulas involving functions of the form f(x) =F(x, e^{h(x)}), where F is an arbitrary bivariate polynomial with integer coefficients.Our algorithms generalize the approach of the well-known procedures to solve the decision problem for formulas involving univariate real polynomials. First, we introduce a suitable notion of Sturm sequence for E-polynomials and  show how to compute effectively, given two E-polynomials f and g, the number of real zeros of f at which g vanishes, at which it is positive and at which it is negative.Then, we present a symbolic algorithm for determining all realizable sign conditions on a finite family of E-polynomials. As a byproduct, we define an effectively computable notion of Thom encoding for the zeros of E-polynomials. Finally, we apply these subroutines to the construction of a symbolic decision procedure with a computable complexity for formulas involving E-polynomials.