TY - GEN

T1 - A Poly-algorithmic Quantifier Elimination Package in Maple

AU - Tonks, Zak

N1 - Publisher Copyright:
© Springer Nature Switzerland AG 2020.

PY - 2020/2/28

Y1 - 2020/2/28

N2 - 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.

AB - 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.

KW - Cylindrical Algebraic Decomposition

KW - Quantifier Elimination

KW - Symbolic computation

KW - Virtual Term Substitution

UR - http://www.scopus.com/inward/record.url?scp=85082132830&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-41258-6_13

DO - 10.1007/978-3-030-41258-6_13

M3 - Chapter in a published conference proceeding

SN - 9783030412579

T3 - Communications in Computer and Information Science

SP - 171

EP - 186

BT - Maple in Mathematics Education and Research - 3rd Maple Conference, MC 2019, Proceedings

A2 - Gerhard, Jürgen

A2 - Kotsireas, Ilias

PB - Springer International Publishing

ER -