Evolutionary Virtual Term Substitution in a Quantifier Elimination system

Zak Tonks

Research output: Chapter or section in a book/report/conference proceedingChapter 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 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
Country/TerritorySwitzerland
CityBern
Period10/07/19 → …

ASJC Scopus subject areas

  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Evolutionary Virtual Term Substitution in a Quantifier Elimination system'. Together they form a unique fingerprint.

Cite this