Quantifier Elimination by Cylindrical Algebraic Decomposition Based on Regular Chains

A quantifier elimination algorithm by cylindrical algebraic decomposition based on regular chains is presented. The main idea is to refine a complex cylindrical tree until the signs of polynomials appearing in the tree are sufficient to distinguish the true and false cells. We report on an implementation of our algorithm in the RegularChains library in Maple and illustrate its effectiveness by examples. Key words: quantifier elimination, cylindrical algebraic decomposition, regular chains, triangular decomposition 1