A Quantifier Elimination Procedure Based on Cylindrical Algebraic Decomposition in SyN RAC

摘要

We have been developing SyN RAC, a toolbox on Maple for solving real algebraic constraints derived from various engineering problems. SyNRAC is used as a core engine on which MATLAB toolboxes are built. We have implemented quantifier elimination (QE) by Collins in which cylindrical algebraic decomposition (CAD) playa a central role. A visualization tool for representing the possible region of an output quantifler-free formula for the two-dimensional case is also added in SyNRAC.