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

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.

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

$\mathrm{QuantifierEliminate}\left(\mathrm{exists}\left(\left[x\&comma;y\&comma;z\right]\&comma;0<xyz\right)\right)$

$\mathrm{true}$

$\mathrm{qf},w≔\mathrm{QuantifierEliminate}\left(\mathrm{exists}\left(\left[x\&comma;y\&comma;z\right]\&comma;0<xyz\right)\&comma;'\mathrm{mode}=\mathrm{breadth}'\&comma;'\mathrm{eagerness}'=1\&comma;'\mathrm{output}=\left[\mathrm{qf}\&comma;\mathrm{witnesses}\right]'\right)$

$\mathrm{qf},w≔\mathrm{true},\left[\left[\mathrm{true}\&comma;z=\frac{1}{2}\&comma;y=\frac{1}{2}\&comma;x=\frac{1}{2}\right]\&comma;\left[\mathrm{true}\&comma;z=\frac{1}{2}\&comma;y=\frac{1}{2}\&comma;x=\frac{1}{2}\right]\&comma;\left[\mathrm{true}\&comma;z=\frac{1}{2}\&comma;y=\mathrm{-2}\&comma;x=\mathrm{-2}\right]\&comma;\left[\mathrm{true}\&comma;z=\mathrm{-2}\&comma;y=\frac{1}{2}\&comma;x=\mathrm{-2}\right]\&comma;\left[\mathrm{true}\&comma;z=\mathrm{-2}\&comma;y=\mathrm{-2}\&comma;x=\frac{1}{2}\right]\&comma;\left[\mathrm{true}\&comma;z=\frac{1}{2}\&comma;y=\frac{1}{2}\&comma;x=\frac{1}{2}\right]\&comma;\left[\mathrm{true}\&comma;z=\frac{1}{2}\&comma;y=\mathrm{-2}\&comma;x=\mathrm{-2}\right]\&comma;\left[\mathrm{true}\&comma;z=\frac{1}{2}\&comma;y=\frac{1}{2}\&comma;x=\frac{1}{2}\right]\&comma;\left[\mathrm{true}\&comma;z=\mathrm{-2}\&comma;y=\frac{1}{2}\&comma;x=\mathrm{-2}\right]\right]$

$\mathrm{expr}≔\mathrm{exists}\left(x\&comma;\mathrm{forall}\left(y\&comma;\mathrm{exists}\left(z\&comma;\mathrm{And}\left(4x^2+x{y}^2-z+\frac{1}{4}=0\&comma;2x+y^{2}z+\frac{1}{2}=0\&comma;x^{2}z-\frac{1}{2}x-y^2=0\right)\right)\right)\right)$

$\mathrm{expr}≔\exists \left(x\&comma;\forall \left(y\&comma;\exists \left(z\&comma;4x^2+x{y}^2-z+\frac{1}{4}=0\wedge 2x+y^{2}z+\frac{1}{2}=0\wedge x^{2}z-\frac{1}{2}x-y^2=0\right)\right)\right)$

$\mathrm{QuantifierEliminate}\left(\mathrm{expr}\right)$

$\mathrm{false}$

$\mathrm{QuantifierEliminate}\left(\mathrm{forall}\left(x\&comma;0<x\Rightarrow 0<x^2\right)\right)$

$\mathrm{true}$

$\mathrm{QuantifierEliminate}\left(\mathrm{forall}\left(x\&comma;0\le x\Rightarrow 0<x^2\right)\right)$

$\mathrm{false}$

$\mathrm{expr}≔\mathrm{exists}\left(\left[v\left[1\right]\&comma;v\left[2\right]\&comma;v\left[3\right]\&comma;v\left[4\right]\&comma;v\left[5\right]\&comma;v\left[6\right]\&comma;v\left[7\right]\&comma;v\left[8\right]\right]\&comma;\mathrm{And}\left(v\left[7\right]<0\&comma;0<v\left[8\right]\&comma;0<v\left[4\right]\&comma;v\left[2\right]v\left[6\right]+v\left[3\right]v\left[8\right]=v\left[4\right]\&comma;v\left[1\right]v\left[5\right]+v\left[3\right]v\left[7\right]=v\left[4\right]\&comma;v\left[6\right]=1\&comma;v\left[5\right]=1\&comma;0<v\left[1\right]\right)\right)$

$\mathrm{expr}≔\exists \left(\left[v_1\&comma;v_2\&comma;v_3\&comma;v_4\&comma;v_5\&comma;v_6\&comma;v_7\&comma;v_8\right]\&comma;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)$

$\mathrm{qf},w,\mathrm{data}≔\mathrm{QuantifierEliminate}\left(\mathrm{expr}\&comma;'\mathrm{output}'=\left['\mathrm{qf}'\&comma;'\mathrm{witnesses}'\&comma;'\mathrm{data}'\right]\right)$

$\mathrm{qf},w,\mathrm{data}≔\mathrm{true},\left[\left[\mathrm{true}\&comma;v_8=\frac{9}{2}\&comma;v_7=-\frac{1}{2}\&comma;v_6=1\&comma;v_5=1\&comma;v_4=\frac{1}{4}\&comma;v_3=\frac{1}{2}\&comma;v_2=\mathrm{-2}\&comma;v_1=\frac{1}{2}\right]\right],\mathrm{QEData\; for}\exists \left(\left[v_1\&comma;v_2\&comma;v_3\&comma;v_4\&comma;v_5\&comma;v_6\&comma;v_7\&comma;v_8\right]\&comma;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)$

The QuantifierElimination:-QuantifierEliminate command was introduced in Maple 2023.

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