Evolutionary Virtual Term Substitution in a Quantifier Elimination system

Zak Tonks

Evolutionary Virtual Term Substitution in a Quantifier Elimination system

Zak Tonks

Department of Computer Science

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

Abstract

Quantifier Elimination over real closed fields (QE) is a topic on the borderline of both the Satisfiability Checking and Symbolic Computation communities, where quantified statements of polynomial constraints may be relevant to solving a Satisfiability Modulo Theory (SMT) problem. Two well known algorithms for QE are Cylindrical Algebraic Decomposition (CAD) and Virtual Term Substitution (VTS). While many softwares implement either or both of these algorithms, they are rarely used together. This paper focuses on new proof of concept methods for incremental and decremental VTS, and briefly explores implications of such methods for a poly-algorithmic system using both VTS and CAD to perform QE.

Original language	English
Title of host publication	CEUR Workshop Proceedings
Subtitle of host publication	4th Workshop on Satisfiability Checking and Symbolic Computation
Editors	J. Abbott, A. Griggio
Publisher	CEUR-WS
Volume	2460
Publication status	Published - 31 Jul 2019
Event	4th Workshop on Satisfiability Checking and Symbolic Computation, SC-Square 2019 - Bern, Switzerland Duration: 10 Jul 2019 → …

Publication series

Name	CEUR Workshop Proceedings
Volume	2460
ISSN (Print)	1613-0073

Conference

Conference	4th Workshop on Satisfiability Checking and Symbolic Computation, SC-Square 2019
Country/Territory	Switzerland
City	Bern
Period	10/07/19 → …

ASJC Scopus subject areas

Computer Science(all)

Cite this

Evolutionary Virtual Term Substitution in a Quantifier Elimination system. / Tonks, Zak.

CEUR Workshop Proceedings: 4th Workshop on Satisfiability Checking and Symbolic Computation. ed. / J. Abbott; A. Griggio. Vol. 2460 CEUR-WS, 2019. (CEUR Workshop Proceedings; Vol. 2460).

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

Tonks, Z 2019, Evolutionary Virtual Term Substitution in a Quantifier Elimination system. in J Abbott & A Griggio (eds), CEUR Workshop Proceedings: 4th Workshop on Satisfiability Checking and Symbolic Computation. vol. 2460, CEUR Workshop Proceedings, vol. 2460, CEUR-WS, 4th Workshop on Satisfiability Checking and Symbolic Computation, SC-Square 2019, Bern, Switzerland, 10/07/19.

@inproceedings{3e667c9236a8410bb964666cc0ea25ba,

title = "Evolutionary Virtual Term Substitution in a Quantifier Elimination system",

abstract = "Quantifier Elimination over real closed fields (QE) is a topic on the borderline of both the Satisfiability Checking and Symbolic Computation communities, where quantified statements of polynomial constraints may be relevant to solving a Satisfiability Modulo Theory (SMT) problem. Two well known algorithms for QE are Cylindrical Algebraic Decomposition (CAD) and Virtual Term Substitution (VTS). While many softwares implement either or both of these algorithms, they are rarely used together. This paper focuses on new proof of concept methods for incremental and decremental VTS, and briefly explores implications of such methods for a poly-algorithmic system using both VTS and CAD to perform QE.",

author = "Zak Tonks",

year = "2019",

month = jul,

day = "31",

language = "English",

volume = "2460",

series = "CEUR Workshop Proceedings",

publisher = "CEUR-WS",

editor = "J. Abbott and A. Griggio",

booktitle = "CEUR Workshop Proceedings",

note = "4th Workshop on Satisfiability Checking and Symbolic Computation, SC-Square 2019 ; Conference date: 10-07-2019",

}

TY - GEN

T1 - Evolutionary Virtual Term Substitution in a Quantifier Elimination system

AU - Tonks, Zak

PY - 2019/7/31

Y1 - 2019/7/31

N2 - Quantifier Elimination over real closed fields (QE) is a topic on the borderline of both the Satisfiability Checking and Symbolic Computation communities, where quantified statements of polynomial constraints may be relevant to solving a Satisfiability Modulo Theory (SMT) problem. Two well known algorithms for QE are Cylindrical Algebraic Decomposition (CAD) and Virtual Term Substitution (VTS). While many softwares implement either or both of these algorithms, they are rarely used together. This paper focuses on new proof of concept methods for incremental and decremental VTS, and briefly explores implications of such methods for a poly-algorithmic system using both VTS and CAD to perform QE.

AB - Quantifier Elimination over real closed fields (QE) is a topic on the borderline of both the Satisfiability Checking and Symbolic Computation communities, where quantified statements of polynomial constraints may be relevant to solving a Satisfiability Modulo Theory (SMT) problem. Two well known algorithms for QE are Cylindrical Algebraic Decomposition (CAD) and Virtual Term Substitution (VTS). While many softwares implement either or both of these algorithms, they are rarely used together. This paper focuses on new proof of concept methods for incremental and decremental VTS, and briefly explores implications of such methods for a poly-algorithmic system using both VTS and CAD to perform QE.

UR - http://www.scopus.com/inward/record.url?scp=85073781667&partnerID=8YFLogxK

M3 - Chapter in a published conference proceeding

AN - SCOPUS:85073781667

VL - 2460

T3 - CEUR Workshop Proceedings

BT - CEUR Workshop Proceedings

A2 - Abbott, J.

A2 - Griggio, A.

PB - CEUR-WS

T2 - 4th Workshop on Satisfiability Checking and Symbolic Computation, SC-Square 2019

Y2 - 10 July 2019

ER -

Evolutionary Virtual Term Substitution in a Quantifier Elimination system

Abstract

Publication series

Conference

ASJC Scopus subject areas

Other files and links

Fingerprint

Cite this