The quantifier elimination (QE) problem is the following: given a formula with polynomial equations and inequalities and quantifiers, construct an equivalent formula (i.e. a formula with the same solution set over ~R) without quantifiers. It has been observed that a broad range of problems in mathematics, computer science, engineering and industrial computations can be reduced to the QE problem (see Loos and Weispfenning, 1993; Gonzalez-Vega, 1998; Hong, 1996; Dorato et al, 1997; Hong, 1997; Weispfenning, 1997).
The first algorithm which is practically useful has been given in Collins (1975), with improvements described in Arnon et al. (1988), Arnon and McCallum (1982), Collins (1998), Collins and Hong (1991), Collins and Johnson (1989), McCallum (1988), Brown (1996), and Brown (1999). Other algorithmic approaches are described in Renegar (1992), Weispfenning (1998), Dolzmann and Sturm (1997), and Gonzalez-Vega (1998).
Many applications, especially in mechanical engineering and in numerical analysis (see Gozalez-Lopez and Recio, 1993; Liska and Steinberg, 1993; Jirstrand, 1997), lead to QE problems with trigonometric functions involved. The general first-order theory of the real numbers with sine and cosine is undecidable: since the zeros of the sine function are precisely the integral multiples of 7Г, one can find Diophantine arithmetic within it, which is undecidable (see also Tarski, 1951). Fortunately, the formulas occurring in any reasonable applications have a more specific structure: the trigonometric (angle) variables are not intermixed with the other variables, and angle variables do not get multiplied with each other. This particular subclass of formulas is decidable. Actually, there are two well-known methods for decision.
