|
Abstract : |
In this paper, we present a decision procedure for certain lineartrigonometric problems for the reals and integers formalized in a suitable rst-order language. The inputs are restricted to formulas, where all but one of the quantied variables occur linearly and at most one occurs both linearly and in a specic trigonometric function. Moreover we allow in addition the integer-part operation in formulas. Besides ordinary quantiers, we allow also counting quantiers. Furthermore we also determine the qualitative structure of the connected components of the satisfaction set of the mixed linear-trigonometric variable. We also consider the decision of these problems in subelds of the real algebraic numbers., |
