A special class of univariate transcendental decision problems called “trigonometric extension” is studied in this paper. Roughly speaking, a trigonometric extension is a ring of univariate analytic functions obtained by adjoining trigonometric functions to a ring consisting of functions having only finitely many real zeros. It is shown that in this case, the decision problem can be reduced to looking for solutions in a bounded domain. Based on the reduction, several new decidability results are established when Schanuel’s Conjecture is assumed. Furthermore, for the theory of multivariate trigonometric extension, it is proved that, although a small fragment of the theory can be reduced to the univariate case, the general theory is undecidable.

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.