  We address the decision problem for sentences involving univariate functions
constructed from a fixed Pfaffian function of order $1$. We present a new
symbolic procedure solving this problem with a computable complexity based on
the computation of suitable Sturm sequences. For a general Pfaffian function,
we assume the existence of an oracle to determine the sign that a function of
the class takes at a real algebraic number. For E-polynomials, we give an
effective algorithm solving the problem without using oracles and apply it to
solve a similar decision problem in the multivariate setting. Finally, we
introduce a notion of Thom encoding for zeros of an E-polynomial and describe
an algorithm for their computation.
