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

QuantifierElimination

 QuantifierEliminate
 perform quantifier elimination on any quantified boolean formula of polynomials via VTS/CAD

 Calling Sequence QuantifierEliminate( expr, opts )

Parameters

 expr - any (quantified) boolean formula of polynomial constraints (a rational Tarski formula) opts - all keyword options applicable to poly-algorithmic QE (described in QuantifierElimination options)

Returns

 • Up to three outputs depending on the value of the keyword option output, described in QuantifierElimination options.

Description

 • Performs Quantifier Elimination (QE) via Virtual Term Substitution (VTS) whenever possible, else (partial) Cylindrical Algebraic Decomposition (CAD) on those intermediate problems that are excessive degree for VTS to compute QE on within a last block of quantified variables.
 • By default and where applicable, the methodology is "poly-algorithmic", if hybmode = depth or breadth, else the methodology is to collapse the whole state of VTS as one QE problem for CAD, as would be the case with other packages.
 • This is in contrast to PartialCylindricalAlgebraicDecompose, which performs all QE purely by partial CAD.
 • The input formula expr need not be prenex, but it is converted to prenex form on input for the purposes of computation.
 • The CAD-related options are only relevant where CAD is used beyond VTS.

Examples

 > $\mathrm{with}\left(\mathrm{QuantifierElimination}\right):$
 > $\mathrm{QuantifierEliminate}\left(\mathrm{exists}\left(\left[x,y,z\right],0
 ${\mathrm{true}}$ (1)

Give a complete set of examples covering all possibilities for witness points for this equivalence:

 > $\mathrm{qf},w≔\mathrm{QuantifierEliminate}\left(\mathrm{exists}\left(\left[x,y,z\right],0
 ${\mathrm{qf}}{,}{w}{≔}{\mathrm{true}}{,}\left[\left[{\mathrm{true}}{,}{z}{=}\frac{{1}}{{2}}{,}{y}{=}\frac{{1}}{{2}}{,}{x}{=}\frac{{1}}{{2}}\right]{,}\left[{\mathrm{true}}{,}{z}{=}\frac{{1}}{{2}}{,}{y}{=}\frac{{1}}{{2}}{,}{x}{=}\frac{{1}}{{2}}\right]{,}\left[{\mathrm{true}}{,}{z}{=}\frac{{1}}{{2}}{,}{y}{=}{-2}{,}{x}{=}{-2}\right]{,}\left[{\mathrm{true}}{,}{z}{=}{-2}{,}{y}{=}\frac{{1}}{{2}}{,}{x}{=}{-2}\right]{,}\left[{\mathrm{true}}{,}{z}{=}{-2}{,}{y}{=}{-2}{,}{x}{=}\frac{{1}}{{2}}\right]{,}\left[{\mathrm{true}}{,}{z}{=}\frac{{1}}{{2}}{,}{y}{=}\frac{{1}}{{2}}{,}{x}{=}\frac{{1}}{{2}}\right]{,}\left[{\mathrm{true}}{,}{z}{=}\frac{{1}}{{2}}{,}{y}{=}{-2}{,}{x}{=}{-2}\right]{,}\left[{\mathrm{true}}{,}{z}{=}\frac{{1}}{{2}}{,}{y}{=}\frac{{1}}{{2}}{,}{x}{=}\frac{{1}}{{2}}\right]{,}\left[{\mathrm{true}}{,}{z}{=}{-2}{,}{y}{=}\frac{{1}}{{2}}{,}{x}{=}{-2}\right]\right]$ (2)
 > $\mathrm{expr}≔\mathrm{exists}\left(x,\mathrm{forall}\left(y,\mathrm{exists}\left(z,\mathrm{And}\left(4{x}^{2}+x{y}^{2}-z+\frac{1}{4}=0,2x+{y}^{2}z+\frac{1}{2}=0,{x}^{2}z-\frac{1}{2}x-{y}^{2}=0\right)\right)\right)\right)$
 ${\mathrm{expr}}{≔}{\exists }{}\left({x}{,}{\forall }{}\left({y}{,}{\exists }{}\left({z}{,}{4}{}{{x}}^{{2}}{+}{x}{}{{y}}^{{2}}{-}{z}{+}\frac{{1}}{{4}}{=}{0}{\wedge }{2}{}{x}{+}{{y}}^{{2}}{}{z}{+}\frac{{1}}{{2}}{=}{0}{\wedge }{{x}}^{{2}}{}{z}{-}\frac{{1}}{{2}}{}{x}{-}{{y}}^{{2}}{=}{0}\right)\right)\right)$ (3)
 > $\mathrm{QuantifierEliminate}\left(\mathrm{expr}\right)$
 ${\mathrm{false}}$ (4)
 > $\mathrm{QuantifierEliminate}\left(\mathrm{forall}\left(x,0
 ${\mathrm{true}}$ (5)
 > $\mathrm{QuantifierEliminate}\left(\mathrm{forall}\left(x,0\le x⇒0<{x}^{2}\right)\right)$
 ${\mathrm{false}}$ (6)

Additionally output witnesses and a QEData object as the further output arguments, where the QE data enables evolutionary computation via InsertFormula and DeleteFormula:

 > $\mathrm{expr}≔\mathrm{exists}\left(\left[v\left[1\right],v\left[2\right],v\left[3\right],v\left[4\right],v\left[5\right],v\left[6\right],v\left[7\right],v\left[8\right]\right],\mathrm{And}\left(v\left[7\right]<0,0
 ${\mathrm{expr}}{≔}{\exists }{}\left(\left[{{v}}_{{1}}{,}{{v}}_{{2}}{,}{{v}}_{{3}}{,}{{v}}_{{4}}{,}{{v}}_{{5}}{,}{{v}}_{{6}}{,}{{v}}_{{7}}{,}{{v}}_{{8}}\right]{,}{{v}}_{{7}}{<}{0}{\wedge }{0}{<}{{v}}_{{8}}{\wedge }{0}{<}{{v}}_{{4}}{\wedge }{{v}}_{{2}}{}{{v}}_{{6}}{+}{{v}}_{{3}}{}{{v}}_{{8}}{=}{{v}}_{{4}}{\wedge }{{v}}_{{1}}{}{{v}}_{{5}}{+}{{v}}_{{3}}{}{{v}}_{{7}}{=}{{v}}_{{4}}{\wedge }{{v}}_{{6}}{=}{1}{\wedge }{{v}}_{{5}}{=}{1}{\wedge }{0}{<}{{v}}_{{1}}\right)$ (7)
 > $\mathrm{qf},w,\mathrm{data}≔\mathrm{QuantifierEliminate}\left(\mathrm{expr},'\mathrm{output}'=\left['\mathrm{qf}','\mathrm{witnesses}','\mathrm{data}'\right]\right)$
 ${\mathrm{qf}}{,}{w}{,}{\mathrm{data}}{≔}{\mathrm{true}}{,}\left[\left[{\mathrm{true}}{,}{{v}}_{{8}}{=}\frac{{9}}{{2}}{,}{{v}}_{{7}}{=}{-}\frac{{1}}{{2}}{,}{{v}}_{{6}}{=}{1}{,}{{v}}_{{5}}{=}{1}{,}{{v}}_{{4}}{=}\frac{{1}}{{4}}{,}{{v}}_{{3}}{=}\frac{{1}}{{2}}{,}{{v}}_{{2}}{=}{-2}{,}{{v}}_{{1}}{=}\frac{{1}}{{2}}\right]\right]{,}{\mathrm{QEData for}}{}{\exists }{}\left(\left[{{v}}_{{1}}{,}{{v}}_{{2}}{,}{{v}}_{{3}}{,}{{v}}_{{4}}{,}{{v}}_{{5}}{,}{{v}}_{{6}}{,}{{v}}_{{7}}{,}{{v}}_{{8}}\right]{,}{{v}}_{{7}}{<}{0}{\wedge }{-}{{v}}_{{8}}{<}{0}{\wedge }{-}{{v}}_{{4}}{<}{0}{\wedge }{{v}}_{{2}}{}{{v}}_{{6}}{+}{{v}}_{{3}}{}{{v}}_{{8}}{-}{{v}}_{{4}}{=}{0}{\wedge }{{v}}_{{1}}{}{{v}}_{{5}}{+}{{v}}_{{3}}{}{{v}}_{{7}}{-}{{v}}_{{4}}{=}{0}{\wedge }{{v}}_{{6}}{-}{1}{=}{0}{\wedge }{{v}}_{{5}}{-}{1}{=}{0}{\wedge }{-}{{v}}_{{1}}{<}{0}\right)$ (8)

Compatibility

 • The QuantifierElimination:-QuantifierEliminate command was introduced in Maple 2023.
 • For more information on Maple 2023 changes, see Updates in Maple 2023.