A Poly-algorithmic Quantifier Elimination Package in Maple

  • Zak TonksEmail author
Conference paper
Part of the Communications in Computer and Information Science book series (CCIS, volume 1125)


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.


Quantifier Elimination Virtual Term Substitution Cylindrical Algebraic Decomposition Symbolic computation 


  1. 1.
    Alvandi, P., Chen, C., Lemaire, F., Maza, M., Xie, Y.: The RegularChains Library.
  2. 2.
    Brown, C.W.: QEPCAD B: a program for computing with semi-algebraic sets using CADs. SIGSAM Bull. 37(4), 97–108 (2003). Scholar
  3. 3.
    Brown, C.W.: Fast simplifications for Tarski formulas based on monomial inequalities. J. Symb. Comput. 47(7), 859–882 (2012). Scholar
  4. 4.
    Brown, C.W., Davenport, J.H.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proceedings of the 2007 International Symposium on Symbolic and Algebraic Computation, ISSAC 2007, pp. 54–60. ACM, New York, NY, USA (2007).
  5. 5.
    Chen, C., Maza, M.M.: Simplification of cylindrical algebraic formulas. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) CASC 2015. LNCS, vol. 9301, pp. 119–134. Springer, Cham (2015). Scholar
  6. 6.
    Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975). Scholar
  7. 7.
    Davenport, J., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1), 29–35 (1988). Scholar
  8. 8.
    England, M., Wilson, D., Bradford, R., Davenport, J.H.: Using the regular chains library to build cylindrical algebraic decompositions by projecting and lifting. In: Hong, H., Yap, C. (eds.) ICMS 2014. LNCS, vol. 8592, pp. 458–465. Springer, Heidelberg (2014). Scholar
  9. 9.
    Hong, H., Collins, G.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 299–328 (1991). Scholar
  10. 10.
    Košta, M.: New concepts for real quantifier elimination by virtual substitution. Ph.D. thesis, Universität des Saarlandes (2016).
  11. 11.
  12. 12.
    McCallum, S.: On projection in CAD-based quantifier elimination with equational constraint. In: Proceedings ISSAC 1999, pp. 145–149 (1999).
  13. 13.
    McCallum, S.: On propagation of equational constraints in CAD-based quantifier elimination. In: Proceedings ISSAC 2001, pp. 223–231 (2001).
  14. 14.
    McCallum, S., Parusiński, A., Paunescu, L.: Validity proof of Lazard’s method for CAD construction. J. Symb. Comput. 92, 52–69 (2019). Scholar
  15. 15.
    Strzebonski, A.: Real Polynomial Systems, Wolfram Mathematica.
  16. 16.
    Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn. Univ. Cal. Press (1951). Reprinted in Quantifier Elimination and Cylindrical Algebraic Decomposition (ed. B.F. Caviness & J.R. Johnson), pp. 24–84. Springer, Wein-New York (1998). Scholar
  17. 17.
    Weispfenning, V.: The complexity of linear problems in fields. J. Symb. Comput. 5(1), 3–27 (1988). Scholar
  18. 18.
    Yanami, H., Anai, H.: SyNRAC: a maple toolbox for solving real algebraic constraints. ACM Commun. Comput. Algebra 41(3), 112–113 (2007). Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.University of BathBathUK

Personalised recommendations