Real Quantifier Elimination in the RegularChains Library

www.csd.uwo.ca/∼moreno Abstract. Quantifier elimination (QE) over real closed fields has found numerous applications. Cylindrical algebraic decomposition (CAD) is one of the main tools for handling quantifier elimination of nonlinear input formulas. Despite of its worst case doubly exponential complexity, CAD-based quantifier elimination remains interesting for handling gen-eral quantified formulas and producing simple quantifier-free formulas. In this paper, we report on the implementation of a QE procedure, called QuantifierElimination, based on the CAD implementations in the Regu-larChains library. This command supports both standard quantifier-free formula and extended Tarski formula in the output. The use of the QE procedure is illustrated by solving examples from different applications