Traditionally, VTS (Virtual Term Substitution) and CAD (Cylindrical Algebraic Decomposition) are the two main algorithms for Quantifier Elimination over the reals (QE) with differing limitations and benefits. We discuss QuantifierElimination, a package in Maple implementing VTS and CAD in a polyalgorithmic sense to attempt to minimise the limitations of both, including an amalgamation of contemporary ideas about CAD including equational constraints & the Lazard projection, providing features in demand for the Real Algebraic Geometry community. Further ideas expand on how best to use CAD following from VTS, including in an incremental sense in the context of QE.
- Quantifier Elimination
- Virtual Term Substitution
- Cylindrical Algebraic Decomposition