ICMS 2020 Session

Real Algebraic Geometry

Accepted Talk

Zak Tonks (University of Bath)
VTS and Lazard Projection CAD in Quantifier Elimination with Maple
Abstract: 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.