Overview - Maple Help

Overview of the QuantifierTools Subpackage

Description

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

List of QuantifierTools Commands

Examples

 > $\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]$ (1)
 > $\mathrm{ConvertToPrenexForm}\left(\mathrm{And}\left(\mathrm{exists}\left(x,x=0\right),\mathrm{exists}\left(x,{x}^{2}<4\right)\right)\right)$
 ${\exists }{}\left(\left[{x}{,}\mathrm{x__1}\right]{,}{x}{=}{0}{\wedge }{\mathrm{x__1}}^{{2}}{<}{4}\right)$ (2)
 > $\mathrm{AlphaConvert}\left(\mathrm{Or}\left(\mathrm{exists}\left(x,x=0\right),\mathrm{exists}\left(x,xy=0\right)\right)\right)$
 ${\exists }{}\left({x}{,}{x}{=}{0}\right){\vee }{\exists }{}\left(\mathrm{x__1}{,}\mathrm{x__1}{}{y}{=}{0}\right)$ (3)
 > $\mathrm{GetAllPolynomials}\left(\mathrm{Or}\left({x}^{2}+5y<0,\mathrm{And}\left({x}^{5}z+y=0,x+z\le 1\right)\right)\right)$
 $\left\{{x}{+}{z}{-}{1}{,}{{x}}^{{2}}{+}{5}{}{y}{,}{{x}}^{{5}}{}{z}{+}{y}\right\}$ (4)

Compatibility

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