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


  • 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