Advertisement

A Poly-algorithmic Quantifier Elimination Package in Maple

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

Abstract

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.

Keywords

Quantifier Elimination Virtual Term Substitution Cylindrical Algebraic Decomposition Symbolic computation 

References

  1. 1.
    Alvandi, P., Chen, C., Lemaire, F., Maza, M., Xie, Y.: The RegularChains Library. http://www.regularchains.org/
  2. 2.
    Brown, C.W.: QEPCAD B: a program for computing with semi-algebraic sets using CADs. SIGSAM Bull. 37(4), 97–108 (2003).  https://doi.org/10.1145/968708.968710CrossRefzbMATHGoogle Scholar
  3. 3.
    Brown, C.W.: Fast simplifications for Tarski formulas based on monomial inequalities. J. Symb. Comput. 47(7), 859–882 (2012).  https://doi.org/10.1016/j.jsc.2011.12.012MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1145/1277548.1277557
  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).  https://doi.org/10.1007/978-3-319-24021-3_9CrossRefGoogle 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).  https://doi.org/10.1007/3-540-07407-4_17CrossRefGoogle Scholar
  7. 7.
    Davenport, J., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1), 29–35 (1988).  https://doi.org/10.1016/S0747-7171(88)80004-XMathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-662-44199-2_69CrossRefGoogle Scholar
  9. 9.
    Hong, H., Collins, G.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 299–328 (1991).  https://doi.org/10.1016/S0747-7171(08)80152-6MathSciNetCrossRefGoogle Scholar
  10. 10.
    Košta, M.: New concepts for real quantifier elimination by virtual substitution. Ph.D. thesis, Universität des Saarlandes (2016).  https://doi.org/10.22028/D291-26679
  11. 11.
  12. 12.
    McCallum, S.: On projection in CAD-based quantifier elimination with equational constraint. In: Proceedings ISSAC 1999, pp. 145–149 (1999).  https://doi.org/10.1145/309831.309892
  13. 13.
    McCallum, S.: On propagation of equational constraints in CAD-based quantifier elimination. In: Proceedings ISSAC 2001, pp. 223–231 (2001).  https://doi.org/10.1145/384101.384132
  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).  https://doi.org/10.1016/j.jsc.2017.12.002MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Strzebonski, A.: Real Polynomial Systems, Wolfram Mathematica. https://reference.wolfram.com/language/tutorial/RealPolynomialSystems.html
  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).  https://doi.org/10.1007/978-3-7091-9459-1_3Google Scholar
  17. 17.
    Weispfenning, V.: The complexity of linear problems in fields. J. Symb. Comput. 5(1), 3–27 (1988).  https://doi.org/10.1016/S0747-7171(88)80003-8MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1145/1358190.1358205CrossRefzbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.University of BathBathUK

Personalised recommendations