VTS and Lazard Projection CAD in Quantifier Elimination with Maple

Zak Tonks

doi:10.5446/48017

VTS and Lazard Projection CAD in Quantifier Elimination with Maple

Zak Tonks

Department of Computer Science

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 language	English
Type	Recorded talk for virtual conference ICMS 2020 (Real Algebraic Geometry session)
Media of output	Recorded Video
Publisher	Technischen Universitat Braunschweig
Place of Publication	TIB AV
DOIs	https://doi.org/10.5446/48017
Publication status	Published - 6 Aug 2020

Keywords

Quantifier Elimination
Virtual Term Substitution
Cylindrical Algebraic Decomposition

Access to Document

10.5446/48017Licence: CC BY-NC-ND

Cite this

@misc{3e458801fee4443bb77d19977b5252b0,

title = "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.",

keywords = "Quantifier Elimination, Virtual Term Substitution, Cylindrical Algebraic Decomposition",

author = "Zak Tonks",

year = "2020",

month = aug,

day = "6",

doi = "10.5446/48017",

language = "English",

publisher = "Technischen Universitat Braunschweig",

address = "Germany",

type = "Other",

}

TY - GEN

T1 - VTS and Lazard Projection CAD in Quantifier Elimination with Maple

AU - Tonks, Zak

PY - 2020/8/6

Y1 - 2020/8/6

N2 - 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.

AB - 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.

KW - Quantifier Elimination

KW - Virtual Term Substitution

KW - Cylindrical Algebraic Decomposition

U2 - 10.5446/48017

DO - 10.5446/48017

M3 - Other contribution

PB - Technischen Universitat Braunschweig

CY - TIB AV

ER -

VTS and Lazard Projection CAD in Quantifier Elimination with Maple

Abstract

Keywords

Access to Document

Fingerprint

Cite this