Evolutionary virtual term substitution in a quantifier elimination system

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish
Title of host publicationCEUR Workshop Proceedings
Subtitle of host publication4th Workshop on Satisfiability Checking and Symbolic Computation
EditorsJ. Abbott, A. Griggio
PublisherCEUR-WS
Volume2460
Publication statusPublished - 31 Jul 2019
Event4th Workshop on Satisfiability Checking and Symbolic Computation, SC-Square 2019 - Bern, Switzerland
Duration: 10 Jul 2019 → …

Publication series

NameCEUR Workshop Proceedings
Volume2460
ISSN (Print)1613-0073

Conference

Conference4th Workshop on Satisfiability Checking and Symbolic Computation, SC-Square 2019
CountrySwitzerland
CityBern
Period10/07/19 → …

ASJC Scopus subject areas

  • Computer Science(all)

Cite this

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.