Quantifier Elimination for Trigonometric Polynomials by Cylindrical Trigonometric Decomposition

Given a formula Φ in r variables, some of them quantified and/or occurring as arguments in trigonometric functions, we consider in this paper the problem of finding a quantifier-free formula equivalent toΦ . We present an algorithm that first computes a decomposition of the space so that the polynomials occurring inΦ are sign-invariant over each cell of this decomposition. Then the cells over which Φ is true are collected: their description gives a quantifier-free formula equivalent to Φ. The algorithm is an adaption of a well-known algorithm for the same problem with polynomial functions.