TY - JOUR
T1 - A Combined VTS/Lazard Quantifier Elimination Method
AU - Davenport, James H.
AU - Tonks, Zak P.
AU - Uncu, Ali K.
N1 - Funding Information:
The authors are grateful to Marek Košta and Jürgen Gerhard for correspondence about Appendix A. The first author would like to thank the EPSRC grant number EP/T015713/1 for supporting his research. The second author would like to thank EPSRC and Maplesoft for funding his research studentship. The third author would like to thank the EPSRC grant number EP/T015713/1 and the FWF grant P-34501N for partially supporting his research.
PY - 2022/12/31
Y1 - 2022/12/31
N2 - Many nonlinear optimisation problems involving systems of multivariate polynomial constraints can be expressed as Quantifier Elimination problems. In this regard, the need to eliminate quantifiers presents itself in many real problems such as in economics, mechanics, and motion planning. We focus on using Cylindrical Algebraic Decomposition and Virtual Term Substitution simultaneously. In this paper, we introduce the state-of-the-art theory behind an implementation of these methods produced in collaboration with Maplesoft.
AB - Many nonlinear optimisation problems involving systems of multivariate polynomial constraints can be expressed as Quantifier Elimination problems. In this regard, the need to eliminate quantifiers presents itself in many real problems such as in economics, mechanics, and motion planning. We focus on using Cylindrical Algebraic Decomposition and Virtual Term Substitution simultaneously. In this paper, we introduce the state-of-the-art theory behind an implementation of these methods produced in collaboration with Maplesoft.
KW - Cylindrical Algebraic Decomposition
KW - Equational Constraints
KW - Quantifier Elimination
KW - Virtual Term Substitution
UR - http://www.scopus.com/inward/record.url?scp=85142876762&partnerID=8YFLogxK
M3 - Conference article
AN - SCOPUS:85142876762
VL - 3273
SP - 41
EP - 49
JO - CEUR Workshop Proceedings
JF - CEUR Workshop Proceedings
SN - 1613-0073
T2 - 6th Satisfiability Checking and Symbolic Computation-Square Workshop, SC-Square 2021
Y2 - 19 August 2021 through 20 August 2021
ER -