A subpackage of QuantifierElimination consisting of procedures for working with Tarski formulae, i.e. quantified boolean formulae of polynomial constraints, which are the input expressions used in quantifier elimination problems (for real closed fields).

These procedures are intended to help one understand the common operations undertaken on these formulae, including to receive "Prenex form" for a formula. AlphaConvert, for example, will help to show when bound variables encounter conflicts within a formula, and so will offer a renaming.

$\mathrm{with}\left(\mathrm{QuantifierElimination}\right)\:$$\mathrm{with}\left(\mathrm{QuantifierTools}\right)$

$\left[\mathrm{AlphaConvert}\,\mathrm{ConvertRationalConstraintsToTarski}\,\mathrm{ConvertToPrenexForm}\,\mathrm{GetAllPolynomials}\,\mathrm{GetEquationalConstraints}\,\mathrm{GetUnquantifiedFormula}\,\mathrm{NegateFormula}\,\mathrm{SuggestCADOptions}\right]$

$\mathrm{ConvertToPrenexForm}\left(\mathrm{And}\left(\mathrm{exists}\left(x\&comma;x=0\right)\&comma;\mathrm{exists}\left(x\&comma;x^2<4\right)\right)\right)$

$\exists \left(\left[x\&comma;\mathrm{x\_\_1}\right]\&comma;x=0\wedge {\mathrm{x\_\_1}}^2<4\right)$

$\mathrm{AlphaConvert}\left(\mathrm{Or}\left(\mathrm{exists}\left(x\&comma;x=0\right)\&comma;\mathrm{exists}\left(x\&comma;xy=0\right)\right)\right)$

$\exists \left(x\&comma;x=0\right)\vee \exists \left(\mathrm{x\_\_1}\&comma;\mathrm{x\_\_1}y=0\right)$

$\mathrm{GetAllPolynomials}\left(\mathrm{Or}\left(x^2+5y<0\&comma;\mathrm{And}\left(x^{5}z+y=0\&comma;x+z\le 1\right)\right)\right)$

$\left\{x+z-1\&comma;x^2+5y\&comma;x^{5}z+y\right\}$

The QuantifierElimination:-QuantifierTools package was introduced in Maple 2023.

For more information on Maple 2023 changes, see Updates in Maple 2023.