VTS and Lazard Projection CAD in Quantifier Elimination with Maple

Research output: Other contribution

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

Keywords

  • Quantifier Elimination
  • Virtual Term Substitution
  • Cylindrical Algebraic Decomposition

Cite this