Deciding Linear-Trigonometric Problems (Theory and Application in Computer Algebra)
Hirokazu Anai, Volker Weispfenning · Institutional Repositories DataBase (IRDB) · 2001
In this paper, we present a decision procedure for certain linear-trigonometric problems for the reals and integers formalized in a suitable first-order language.The inputs are restricted to formulas, where all but one of the quantified variables occur linearly and at most one occurs both linearly and in a specific trigonometric function.Moreover we allow in addition the integer-part operation in formulas.Besides ordinary quantifiers, we allow also counting quantifiers.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 subfields of the real algebraic numbers.complexity.A more efficient alternative was proposed, by Pau et al.; it adapts Collins' CAD