Deciding first-order formulas involving univariate mixed trigonometric-polynomials

A decision algorithm for the first-order theory of univariate mixed trigonometric-polynomials over the reals is proposed in this paper. In the development of the decision algorithm, the concept "contraction mapping associated with an algebraic function" is introduced and a new real root isolation algorithm for univariate mixed trigonometric-polynomials is presented. The decision algorithm is implemented with Mathematica and its effectiveness is shown by some experimental results.