Quantifier elimination for trigonometric polynomials by cylindrical trigonometric decomposition (Q1581134)

The authors present a quantifier elimination algorithm for some first-order formulas involving the trigonometric functions sine and cosine based on the cylindrical algebraic decomposition of semi-algebraic sets due to Collin (see \textit{G. E. Collins}, Lect. Notes Comput. Sci. 33, 134-183 (1975; Zbl 0318.02051)). There are two well-known methods to extend the algebraic elimination procedures to formulas containing trigonometric functions: either introducing new variables for \(s_i= \sin(x_i)\) and \(c_i= \cos(x_i)\) and adding the conditions \(s^2_i+ c^2_i= 1\) or expressing all trigonometric functions in \(\tan({x_i\over 2})\) and introducing new variables \(t_i= \tan({x_i\over 2})\). The authors use this second method as it introduces fewer new variables. To deal algorithmically with the possible indefinitions of the tangent, they give a cylindrical trigonometric decomposition of the space, which is not algebraic anymore and makes the complexity of their algorithm lower than the known complexities of algorithms solving the same task.