Quantifier elimination for trigonometric polynomials by cylindrical trigonometric decomposition (Q1581134)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Quantifier elimination for trigonometric polynomials by cylindrical trigonometric decomposition |
scientific article |
Statements
Quantifier elimination for trigonometric polynomials by cylindrical trigonometric decomposition (English)
0 references
1 March 2001
0 references
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.
0 references
quantifier elimination algorithm
0 references
cylindrical trigonometric decomposition
0 references
0 references
0 references
0 references
0 references