Tags:First-Order Formula Decision, Mixed Trigonometric-Polynomial, Real Root Isolation and Transcendental Equations
Abstract:
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 \textsc{Mathematica} and its effectiveness is shown by some experimental results.