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.
展开▼
