VTS and Lazard Projection CAD in Quantifier Elimination with Maple

Zak Tonks

Research output: Other contribution


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.
Original languageEnglish
TypeRecorded talk for virtual conference ICMS 2020 (Real Algebraic Geometry session)
Media of outputRecorded Video
PublisherTechnischen Universitat Braunschweig
Place of PublicationTIB AV
Publication statusPublished - 6 Aug 2020


  • Quantifier Elimination
  • Virtual Term Substitution
  • Cylindrical Algebraic Decomposition


Dive into the research topics of 'VTS and Lazard Projection CAD in Quantifier Elimination with Maple'. Together they form a unique fingerprint.

Cite this