A Poly-algorithmic Quantifier Elimination Package in Maple

Zak Tonks

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

5 Citations (SciVal)


The problem of Quantifier Elimination (QE) in Computer Algebra is that of eliminating all quantifiers from a statement featuring polynomial constraints. This problem is known to be worst case time complexity worst case doubly exponential in the number of variables. As such implementations are sometimes seen as undesirable to use, despite problems arising in algebraic geometry and even economics lending themselves to formulations as QE problems. This paper largely concerns discussion of current progress of a package QuantifierElimination written using Maple that uses a poly-algorithm between two well known algorithms to solve QE: Virtual Term Substitution (VTS), and Cylindrical Algebraic Decomposition (CAD). While mitigation of efficiency concerns is the main aim of the implementation, said implementation being built in Maple reconciles with an aim of providing rich output to users to make use of algorithms to solve QE valuable. We explore the challenges and scope such an implementation gives in terms of the desires of the Satisfiability Modulo Theory (SMT) community, and other frequent uses of QE, noting Maple’s status as a Mathematical toolbox.
Original languageEnglish
Title of host publicationMaple in Mathematics Education and Research - 3rd Maple Conference, MC 2019, Proceedings
EditorsJürgen Gerhard, Ilias Kotsireas
PublisherSpringer International Publishing
Number of pages16
ISBN (Print)9783030412579
Publication statusPublished - 28 Feb 2020

Publication series

NameCommunications in Computer and Information Science
Volume1125 CCIS
ISSN (Print)1865-0929
ISSN (Electronic)1865-0937

Bibliographical note

Publisher Copyright:
© Springer Nature Switzerland AG 2020.


  • Cylindrical Algebraic Decomposition
  • Quantifier Elimination
  • Symbolic computation
  • Virtual Term Substitution

ASJC Scopus subject areas

  • General Computer Science
  • General Mathematics


Dive into the research topics of 'A Poly-algorithmic Quantifier Elimination Package in Maple'. Together they form a unique fingerprint.

Cite this