Example Worksheet - Maple Help
For the best experience, we recommend viewing online help using Google Chrome or Microsoft Edge.

Demonstration of the QuantifierElimination and QuantifierTools packages in Maple

 > with( QuantifierElimination );
 $\left[{\mathrm{CylindricalAlgebraicDecompose}}{,}{\mathrm{DeleteFormula}}{,}{\mathrm{InsertFormula}}{,}{\mathrm{PartialCylindricalAlgebraicDecompose}}{,}{\mathrm{QuantifierEliminate}}{,}{\mathrm{QuantifierTools}}\right]$ (1)
 > with( QuantifierTools );
 $\left[{\mathrm{AlphaConvert}}{,}{\mathrm{ConvertRationalConstraintsToTarski}}{,}{\mathrm{ConvertToPrenexForm}}{,}{\mathrm{GetAllPolynomials}}{,}{\mathrm{GetEquationalConstraints}}{,}{\mathrm{GetUnquantifiedFormula}}{,}{\mathrm{NegateFormula}}{,}{\mathrm{SuggestCADOptions}}\right]$ (2)

This worksheet is an in-depth demonstration of ways to use the routines of QuantifierElimination and QuantifierTools.

Throughout, QE and CAD are abbreviations of Quantifier Elimination and Cylindrical Algebraic Decomposition, respectively.

It also offers a wealth of typical examples on how to interact with QEData and CADData objects returned in the course of incrementality or stock CAD.

QE or CAD formulae as examples that originally have an academic source are appended with a reference on formula definition (generally [3] or [9]). Both works are either repositories of data or works that cite a repository of data. Other references appended at the bottom of the worksheet are general major works of interest in terms of implementation of the QuantifierElimination package. An extremely comprehensive source of reference for the package and in particular its implementation is [8].