The command QuantifierElimination(f) returns a quantifier-free logic formula  $\mathrm{qff}$ logically equivalent to f.

The user interface of Quantifier Elimination relies on the features of the Logic package. In addition to those features, we denote by &E the existential quantifier $\exists$ and by &A the universal quantifier $\forall$.

Extended Tarski formulas are supported with the option output=rootof.

The output formulas can be simplified using different levels of heuristical optimizations, from the lower-level simplification = L1 to the higher-level simplification = L4.

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

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

$f≔\&E\left(\left[c\right]\right),\&A\left(\left[b\,a\right]\right),\left(\left(\left(a=d\right)\&and\left(b=c\right)\right)\&or\left(\left(a=c\right)\&and\left(b=1\right)\right)\right)\&implies\left(a^2=b\right)$

$f≔\&E\left(\left[c\right]\right),\&A\left(\left[b\,a\right]\right),\left(\left(\left(a=d\right)\&and\left(b=c\right)\right)\&or\left(\left(a=c\right)\&and\left(b=1\right)\right)\right)\&implies\left(a^2=b\right)$

$\mathrm{out}≔\mathrm{QuantifierElimination}\left(f\right)$

$\mathrm{out}≔\left(d-1=0\right)\&or\left(d+1=0\right)$

$R≔\mathrm{PolynomialRing}\left(\left[x\,a\,b\,c\right]\right)$

$R≔\mathrm{polynomial\_ring}$

$f≔\&E\left(\left[x\right]\right),a{x}^2+bx+c=0$

$f≔\&E\left(\left[x\right]\right),a{x}^2+bx+c=0$

$\mathrm{out}≔\mathrm{QuantifierElimination}\left(f\,R\right)$

$\mathrm{out}≔\mathrm{\&or}\left(c=0\&comma;\mathrm{\&and}\left(c<0\&comma;b<0\&comma;a=0\right)\&comma;\mathrm{\&and}\left(c<0\&comma;b<0\&comma;0<a\right)\&comma;\mathrm{\&and}\left(c<0\&comma;b<0\&comma;4ac-b^2=0\right)\&comma;\mathrm{\&and}\left(c<0\&comma;b<0\&comma;a<0\&comma;4ac-b^2<0\right)\&comma;\mathrm{\&and}\left(c<0\&comma;b=0\&comma;0<a\right)\&comma;\mathrm{\&and}\left(c<0\&comma;0<b\&comma;a=0\right)\&comma;\mathrm{\&and}\left(c<0\&comma;0<b\&comma;0<a\right)\&comma;\mathrm{\&and}\left(c<0\&comma;0<b\&comma;4ac-b^2=0\right)\&comma;\mathrm{\&and}\left(c<0\&comma;0<b\&comma;a<0\&comma;4ac-b^2<0\right)\&comma;\mathrm{\&and}\left(0<c\&comma;b<0\&comma;a<0\right)\&comma;\mathrm{\&and}\left(0<c\&comma;b<0\&comma;a=0\right)\&comma;\mathrm{\&and}\left(0<c\&comma;b<0\&comma;4ac-b^2=0\right)\&comma;\mathrm{\&and}\left(0<c\&comma;b<0\&comma;0<a\&comma;4ac-b^2<0\right)\&comma;\mathrm{\&and}\left(0<c\&comma;b=0\&comma;a<0\right)\&comma;\mathrm{\&and}\left(0<c\&comma;0<b\&comma;a<0\right)\&comma;\mathrm{\&and}\left(0<c\&comma;0<b\&comma;a=0\right)\&comma;\mathrm{\&and}\left(0<c\&comma;0<b\&comma;4ac-b^2=0\right)\&comma;\mathrm{\&and}\left(0<c\&comma;0<b\&comma;0<a\&comma;4ac-b^2<0\right)\right)$

$f≔\&E\left(\left[x\right]\right),a{x}^2+bx+c=0$

$f≔\&E\left(\left[x\right]\right),x^{2}a+xb+c=0$

$\mathrm{out}≔\mathrm{QuantifierElimination}\left(f\&comma;'\mathrm{output}'='\mathrm{rootof}'\right)$

$\mathrm{out}≔\mathrm{\&or}\left(\left(a<0\right)\&and\left(\frac{b^2}{4a}\le c\right)\&comma;\left(a=0\right)\&and\left(b\ne 0\right)\&comma;\mathrm{\&and}\left(a=0\&comma;b=0\&comma;c=0\right)\&comma;\left(0<a\right)\&and\left(c\le \frac{b^2}{4a}\right)\right)$

$f≔\&E\left(\left[y\right]\right),y^2+x^2=2$

$f≔\&E\left(\left[y\right]\right),x^2+y^2=2$

$\mathrm{out}≔\mathrm{QuantifierElimination}\left(f\&comma;\mathrm{output}=\mathrm{rootof}\right)$

$\mathrm{out}≔\left(-\sqrt{2}\le x\right)\&and\left(x\le \sqrt{2}\right)$

$f≔\&E\left(\left[y\right]\right),y^4+x^4=2$

$f≔\&E\left(\left[y\right]\right),x^4+y^4=2$

$\mathrm{out}≔\mathrm{QuantifierElimination}\left(f\&comma;\mathrm{output}=\mathrm{rootof}\right)$

$\mathrm{out}≔\left(\mathrm{RootOf}\left({\mathrm{\_Z}}^4-2\&comma;\mathrm{index}={\mathrm{real}}_1\right)\le x\right)\&and\left(x\le \mathrm{RootOf}\left({\mathrm{\_Z}}^4-2\&comma;\mathrm{index}={\mathrm{real}}_2\right)\right)$

$\mathrm{ff}≔\&E\left(\left[i\&comma;j\right]\right),\left(\left(\left(\left(0\le i\&andi\le n\right)\&and0\le j\right)\&andj\le n\right)\&and\left(t=n-j\right)\right)\&and\left(p=i+j\right)$

$\mathrm{ff}≔\&E\left(\left[i\&comma;j\right]\right),\left(\left(\left(\left(\left(0\le i\right)\&and\left(i\le n\right)\right)\&and\left(0\le j\right)\right)\&and\left(j\le n\right)\right)\&and\left(t=n-j\right)\right)\&and\left(p=i+j\right)$

$R≔\mathrm{PolynomialRing}\left(\left[i\&comma;j\&comma;p\&comma;t\&comma;n\right]\right)$

$R≔\mathrm{polynomial\_ring}$

$\mathrm{sols}≔\mathrm{QuantifierElimination}\left(\mathrm{ff}\&comma;R\&comma;\mathrm{output}=\mathrm{rootof}\&comma;\mathrm{simplification}=\mathrm{false}\right)$

$\mathrm{sols}≔\mathrm{\&or}\left(\mathrm{\&and}\left(n=0\&comma;t=n\&comma;p=0\right)\&comma;\mathrm{\&and}\left(0<n\&comma;t=0\&comma;p=n\right)\&comma;\mathrm{\&and}\left(0<n\&comma;t=0\&comma;n<p\&comma;p<2n\right)\&comma;\mathrm{\&and}\left(0<n\&comma;t=0\&comma;p=2n\right)\&comma;\mathrm{\&and}\left(0<n\&comma;0<t\&comma;t<n\&comma;p=-t+n\right)\&comma;\mathrm{\&and}\left(0<n\&comma;0<t\&comma;t<n\&comma;-t+n<p\&comma;p<-t+2n\right)\&comma;\mathrm{\&and}\left(0<n\&comma;0<t\&comma;t<n\&comma;p=-t+2n\right)\&comma;\mathrm{\&and}\left(0<n\&comma;t=n\&comma;p=0\right)\&comma;\mathrm{\&and}\left(0<n\&comma;t=n\&comma;0<p\&comma;p<n\right)\&comma;\mathrm{\&and}\left(0<n\&comma;t=n\&comma;p=n\right)\right)$

$\mathrm{sols}≔\mathrm{QuantifierElimination}\left(\mathrm{ff}\&comma;R\&comma;\mathrm{output}=\mathrm{rootof}\&comma;\mathrm{simplification}=\mathrm{L4}\right)$

$\mathrm{sols}≔\mathrm{\&and}\left(0\le n\&comma;0\le t\&comma;t\le n\&comma;n-t\le p\&comma;p\le -t+2n\right)$

Changbo Chen, Marc Moreno Maza "An Incremental Algorithm for Computing Cylindrical Algebraic Decomposition." Proceedings of ASCM 2012, Computer Mathematics, Springer, (2014): 199-221.

Changbo Chen, Marc Moreno Maza "Quantifier elimination by cylindrical algebraic decomposition based on regular chain." J. Symb. Comput. 75: 74-93 (2016)

Changbo Chen, Marc Moreno Maza "Simplification of Cylindrical Algebraic Formula." Computer Algebra in Scientific Computing (CASC), Lecture Notes in Computer Science - 9301, (2015): 119-134.

The RegularChains[SemiAlgebraicSetTools][QuantifierElimination] command was introduced in Maple 2020.

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