A Poly-algorithmic Approach to Quantifier Elimination

Cylindrical Algebraic Decomposition (CAD) was the first practical means for doing Real Quantifier Elimination (QE), and is still a major method. Nevertheless, its complexity is inherently doubly exponential in the number of variables. Where applicable, virtual term substitution (VTS) is more effecti...

Full description

Saved in:
Bibliographic Details
Main Authors: Davenport, James H., Tonks, Zak P., Uncu, Ali K.
Format: Conference Proceeding
Language:English
Subjects:
Complexity theory
Constraint handling
Cylindrical Algebraic Decomposition
Quantifier Elimination
Scientific computing
Turning
Virtual Term Substitution
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Cylindrical Algebraic Decomposition (CAD) was the first practical means for doing Real Quantifier Elimination (QE), and is still a major method. Nevertheless, its complexity is inherently doubly exponential in the number of variables. Where applicable, virtual term substitution (VTS) is more effective, turning a QE problem in n variables to one in n-1 variables in one application, and so on. Hence there is scope for hybrid methods: doing VTS where possible then using CAD. This paper describes such a poly-algorithmic implementation, based on the second author's Ph.D. thesis. The version of CAD used is based on a new implementation of Lazard's method, with improvements to handle equational constraints, similar to the equational constraint handling in previous CAD algorithms.
ISSN:2470-881X
DOI:10.1109/SYNASC61333.2023.00013