A Poly-algorithmic Approach to Quantifier Elimination

James H. Davenport; Zak P. Tonks; Ali K. Uncu

doi:10.1109/SYNASC61333.2023.00013

A Poly-algorithmic Approach to Quantifier Elimination

James H. Davenport, Zak P. Tonks, Ali K. Uncu

The Research Center for Molecular Medicine (CeMM) of the Austrian Academy of Sciences (OeAW)

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

Abstract

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.

Original language	English
Title of host publication	Proceedings - 2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023
Editors	Sorin Stratulat, Mircea Marin, Viorel Negru, Daniela Zaharie
Place of Publication	U. S. A.
Publisher	IEEE
Pages	44-51
Number of pages	8
ISBN (Electronic)	9798350394122
ISBN (Print)	9798350394139
DOIs	https://doi.org/10.1109/SYNASC61333.2023.00013
Publication status	Published - 10 May 2024
Event	25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023 - Nancy, France Duration: 11 Sept 2023 → 14 Sept 2023

Publication series

Name	Proceedings - 2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023

Conference

Conference	25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023
Country/Territory	France
City	Nancy
Period	11/09/23 → 14/09/23

Keywords

Cylindrical Algebraic Decomposition
Quantifier Elimination
Virtual Term Substitution

ASJC Scopus subject areas

Computational Theory and Mathematics
Computer Science Applications
Software
Numerical Analysis
Computational Mathematics
Health Informatics

Access to Document

10.1109/SYNASC61333.2023.00013

Cite this

Davenport, J. H., Tonks, Z. P., & Uncu, A. K. (2024). A Poly-algorithmic Approach to Quantifier Elimination. In S. Stratulat, M. Marin, V. Negru, & D. Zaharie (Eds.), Proceedings - 2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023 (pp. 44-51). (Proceedings - 2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023). IEEE. https://doi.org/10.1109/SYNASC61333.2023.00013

A Poly-algorithmic Approach to Quantifier Elimination. / Davenport, James H.; Tonks, Zak P.; Uncu, Ali K.
Proceedings - 2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023. ed. / Sorin Stratulat; Mircea Marin; Viorel Negru; Daniela Zaharie. U. S. A.: IEEE, 2024. p. 44-51 (Proceedings - 2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023).

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

Davenport, JH, Tonks, ZP & Uncu, AK 2024, A Poly-algorithmic Approach to Quantifier Elimination. in S Stratulat, M Marin, V Negru & D Zaharie (eds), Proceedings - 2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023. Proceedings - 2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023, IEEE, U. S. A., pp. 44-51, 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023, Nancy, France, 11/09/23. https://doi.org/10.1109/SYNASC61333.2023.00013

Davenport JH, Tonks ZP, Uncu AK. A Poly-algorithmic Approach to Quantifier Elimination. In Stratulat S, Marin M, Negru V, Zaharie D, editors, Proceedings - 2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023. U. S. A.: IEEE. 2024. p. 44-51. (Proceedings - 2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023). Epub 2024 May 10. doi: 10.1109/SYNASC61333.2023.00013

Davenport, James H. ; Tonks, Zak P. ; Uncu, Ali K. / A Poly-algorithmic Approach to Quantifier Elimination. Proceedings - 2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023. editor / Sorin Stratulat ; Mircea Marin ; Viorel Negru ; Daniela Zaharie. U. S. A. : IEEE, 2024. pp. 44-51 (Proceedings - 2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023).

@inproceedings{0925fbc5b2184a479698648192234d12,

title = "A Poly-algorithmic Approach to Quantifier Elimination",

abstract = "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.",

keywords = "Cylindrical Algebraic Decomposition, Quantifier Elimination, Virtual Term Substitution",

author = "Davenport, {James H.} and Tonks, {Zak P.} and Uncu, {Ali K.}",

year = "2024",

month = may,

day = "10",

doi = "10.1109/SYNASC61333.2023.00013",

language = "English",

isbn = "9798350394139",

series = "Proceedings - 2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023",

publisher = "IEEE",

pages = "44--51",

editor = "Sorin Stratulat and Mircea Marin and Viorel Negru and Daniela Zaharie",

booktitle = "Proceedings - 2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023",

address = "USA United States",

note = "25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023 ; Conference date: 11-09-2023 Through 14-09-2023",

}

TY - GEN

T1 - A Poly-algorithmic Approach to Quantifier Elimination

AU - Davenport, James H.

AU - Tonks, Zak P.

AU - Uncu, Ali K.

PY - 2024/5/10

Y1 - 2024/5/10

N2 - 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.

AB - 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.

KW - Cylindrical Algebraic Decomposition

KW - Quantifier Elimination

KW - Virtual Term Substitution

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

U2 - 10.1109/SYNASC61333.2023.00013

DO - 10.1109/SYNASC61333.2023.00013

M3 - Chapter in a published conference proceeding

AN - SCOPUS:85193843971

SN - 9798350394139

T3 - Proceedings - 2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023

SP - 44

EP - 51

BT - Proceedings - 2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023

A2 - Stratulat, Sorin

A2 - Marin, Mircea

A2 - Negru, Viorel

A2 - Zaharie, Daniela

PB - IEEE

CY - U. S. A.

T2 - 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023

Y2 - 11 September 2023 through 14 September 2023

ER -

A Poly-algorithmic Approach to Quantifier Elimination

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Dataset for Quantifier Elimination and CAD examples in Maple

Cite this

A Poly-algorithmic Approach to Quantifier Elimination

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Datasets

Dataset for Quantifier Elimination and CAD examples in Maple

Cite this