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)