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.

Original languageEnglish
Pages (from-to)41-49
Number of pages9
JournalCEUR Workshop Proceedings
Publication statusPublished - 31 Dec 2022
Event6th Satisfiability Checking and Symbolic Computation-Square Workshop, SC-Square 2021 - Virtual, Online, USA United States
Duration: 19 Aug 202120 Aug 2021

Bibliographical note

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.


  • Cylindrical Algebraic Decomposition
  • Equational Constraints
  • Quantifier Elimination
  • Virtual Term Substitution

ASJC Scopus subject areas

  • Computer Science(all)


Dive into the research topics of 'A Combined VTS/Lazard Quantifier Elimination Method'. Together they form a unique fingerprint.

Cite this