The QuantifierElimination package has been added in Maple 2023. This package offers a new set of routines for quantifier elimination over the reals (QE). This package is the first package included with Maple to offer Virtual Term Substitution (VTS) as an algorithm for QE. Furthermore it offers a new implementation of Cylindrical Algebraic Decomposition (CAD) being the first implementation using the Lazard projection with equational constraints as part of CAD both for QE and standalone CADs to explore real algebraic geometry. Lastly, a new poly-algorithm offers a new way to use VTS in conjunction with CAD for QE including in incremental contexts.

QuantifierEliminate is the standard routine for elimination:

with(QuantifierElimination);

$\left[\mathrm{CylindricalAlgebraicDecompose}\,\mathrm{DeleteFormula}\,\mathrm{InsertFormula}\,\mathrm{PartialCylindricalAlgebraicDecompose}\,\mathrm{QuantifierEliminate}\,\mathrm{QuantifierTools}\right]$

expr := exists( x, forall( y, exists( z, And(4*x^2 + x*y^2 - z + 1/4 = 0, 2*x + y^2*z + 1/2 = 0, x^2*z - 1/2*x - y^2 = 0 ) ) ) );

$\mathrm{expr}≔\exists \left(x\,\forall \left(y\,\exists \left(z\,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)$

QuantifierEliminate(expr);

$\mathrm{false}$

You can opt to include with the result witnesses that prove equivalence of quantifier-free formulae to a quantified expression:

expr := exists([v__1, v__2, v__3, v__4, v__5, v__6, v__7, v__8],And(v__7 < 0,0 < v__8,0 < v__4,v__2*v__6+v__3*v__8 = v__4,v__1*v__5+v__3*v__7 = v__4,v__6 = 1,v__5 = 1, 0 < v__1));

$\mathrm{expr}≔\exists \left(\left[\mathrm{v\_\_1}\&comma;\mathrm{v\_\_2}\&comma;\mathrm{v\_\_3}\&comma;\mathrm{v\_\_4}\&comma;\mathrm{v\_\_5}\&comma;\mathrm{v\_\_6}\&comma;\mathrm{v\_\_7}\&comma;\mathrm{v\_\_8}\right]\&comma;\mathrm{v\_\_7}<0\wedge 0<\mathrm{v\_\_8}\wedge 0<\mathrm{v\_\_4}\wedge \mathrm{v\_\_2}\mathrm{v\_\_6}+\mathrm{v\_\_3}\mathrm{v\_\_8}=\mathrm{v\_\_4}\wedge \mathrm{v\_\_1}\mathrm{v\_\_5}+\mathrm{v\_\_3}\mathrm{v\_\_7}=\mathrm{v\_\_4}\wedge \mathrm{v\_\_6}=1\wedge \mathrm{v\_\_5}=1\wedge 0<\mathrm{v\_\_1}\right)$

(qf, witnesses) := QuantifierEliminate( expr, 'output = [ qf, witnesses]' );

$\mathrm{qf},\mathrm{witnesses}≔\mathrm{true},\left[\left[\mathrm{true}\&comma;\mathrm{v\_\_8}=\frac{9}{2}\&comma;\mathrm{v\_\_7}=-\frac{1}{2}\&comma;\mathrm{v\_\_6}=1\&comma;\mathrm{v\_\_5}=1\&comma;\mathrm{v\_\_4}=\frac{1}{4}\&comma;\mathrm{v\_\_3}=\frac{1}{2}\&comma;\mathrm{v\_\_2}=\mathrm{-2}\&comma;\mathrm{v\_\_1}=\frac{1}{2}\right]\right]$

map(evalb,eval(op(2,expr),witnesses[1][2..-1]));

$\mathrm{true}\wedge \mathrm{true}\wedge \mathrm{true}\wedge \mathrm{true}\wedge \mathrm{true}\wedge \mathrm{true}\wedge \mathrm{true}\wedge \mathrm{true}$

PartialCylindricalAlgebraicDecompose offers QE purely via partial CAD:

expr := exists(c,forall([b, a],Implies(Or(And(a-d = 0,b-c = 0),And(a-c = 0,b-1 = 0)),a^2-b = 0)));

$\mathrm{expr}≔\exists \left(c\&comma;\forall \left(\left[b\&comma;a\right]\&comma;\left(a-d=0\wedge b-c=0\right)\vee \left(a-c=0\wedge b-1=0\right)\Rightarrow a^2-b=0\right)\right)$

PartialCylindricalAlgebraicDecompose(expr);

$d=\mathrm{-1}\vee d=1$

QuantifierTools is a subpackage of QuantifierElimination that offers tools for working with and manipulating Tarski formulae:

with(QuantifierTools);

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

uqf := GetUnquantifiedFormula( expr );

$\mathrm{uqf}≔\left(a-d=0\wedge b-c=0\right)\vee \left(a-c=0\wedge b-1=0\right)\Rightarrow a^2-b=0$

CylindricalAlgebraicDecompose offers production of CADData objects that can be inspected to explore a cylindrical algebraic decomposition:

C := CylindricalAlgebraicDecompose( GetUnquantifiedFormula( expr ), 'variablestrategy' = [ d, c, b, a ] );

$C≔\left[\begin{array}{lll}\mathrm{Variables}& \&equals;& \left[d\&comma;c\&comma;b\&comma;a\right]\\ \mathrm{Input\; Polynomials}& \&equals;& \left[\begin{array}{cccccccccccccccccc}b& c& d& a-c& a-d& b-1& b-c& c-1& c+1& c+d& -d+c& d-1& d+1& -c^2+b& -d^2+b& -d^2+c& d^2+1& a^2-b\end{array}\right]\\ \mathrm{\#\; Cells}& \&equals;& 4949\\ \mathrm{Projection\; polynomials\; for\; level\; 1}& \&equals;& \left[\begin{array}{cccc}d& d-1& d+1& d^2+1\end{array}\right]\\ \mathrm{Projection\; polynomials\; for\; level\; 2}& \&equals;& \left[\begin{array}{cccccc}c& c-1& c+1& c+d& -d+c& -d^2+c\end{array}\right]\\ \mathrm{Projection\; polynomials\; for\; level\; 3}& \&equals;& \left[\begin{array}{ccccc}b& b-1& b-c& -c^2+b& -d^2+b\end{array}\right]\\ \mathrm{Projection\; polynomials\; for\; level\; 4}& \&equals;& \left[\begin{array}{ccc}a-c& a-d& a^2-b\end{array}\right]\end{array}\right.$

leaves := GetLeafCells( C )[ 1 .. 5 ];

$\mathrm{leaves}≔\left[\left[\begin{array}{lll}\mathrm{Description}& \&equals;& 1<d\wedge d^2<c\wedge c^2<b\wedge \mathrm{RootOf}\left({\mathrm{\_Z}}^2-b\&comma;\mathrm{index}={\mathrm{real}}_2\right)<a\\ \mathrm{Sample\; Point}& \&equals;& \left[d=2\&comma;c=5\&comma;b=26\&comma;a=7\right]\\ \mathrm{Index}& \&equals;& \left[7\&comma;13\&comma;11\&comma;9\right]\end{array}\right.\&comma;\left[\begin{array}{lll}\mathrm{Description}& \&equals;& 1<d\wedge d^2<c\wedge c^2<b\wedge a=\mathrm{RootOf}\left({\mathrm{\_Z}}^2-b\&comma;\mathrm{index}={\mathrm{real}}_2\right)\\ \mathrm{Sample\; Point}& \&equals;& \left[d=2\&comma;c=5\&comma;b=26\&comma;a=\mathrm{RootOf}\left({\mathrm{\_Z}}^2-26\&comma;\frac{48158877692977696785785}{9444732965739290427392}..\frac{24079438846488848392933}{4722366482869645213696}\right)\right]\\ \mathrm{Index}& \&equals;& \left[7\&comma;13\&comma;11\&comma;8\right]\end{array}\right.\&comma;\left[\begin{array}{lll}\mathrm{Description}& \&equals;& 1<d\wedge d^2<c\wedge c^2<b\wedge c<a\wedge a<\mathrm{RootOf}\left({\mathrm{\_Z}}^2-b\&comma;\mathrm{index}={\mathrm{real}}_2\right)\\ \mathrm{Sample\; Point}& \&equals;& \left[d=2\&comma;c=5\&comma;b=26\&comma;a=\frac{61}{12}\right]\\ \mathrm{Index}& \&equals;& \left[7\&comma;13\&comma;11\&comma;7\right]\end{array}\right.\&comma;\left[\begin{array}{lll}\mathrm{Description}& \&equals;& 1<d\wedge d^2<c\wedge c^2<b\wedge a=c\\ \mathrm{Sample\; Point}& \&equals;& \left[d=2\&comma;c=5\&comma;b=26\&comma;a=5\right]\\ \mathrm{Index}& \&equals;& \left[7\&comma;13\&comma;11\&comma;6\right]\end{array}\right.\&comma;\left[\begin{array}{lll}\mathrm{Description}& \&equals;& 1<d\wedge d^2<c\wedge c^2<b\wedge d<a\wedge a<c\\ \mathrm{Sample\; Point}& \&equals;& \left[d=2\&comma;c=5\&comma;b=26\&comma;a=3\right]\\ \mathrm{Index}& \&equals;& \left[7\&comma;13\&comma;11\&comma;5\right]\end{array}\right.\right]$

cell := leaves[1];

$\mathrm{cell}≔\left[\begin{array}{lll}\mathrm{Description}& \&equals;& 1<d\wedge d^2<c\wedge c^2<b\wedge \mathrm{RootOf}\left({\mathrm{\_Z}}^2-b\&comma;\mathrm{index}={\mathrm{real}}_2\right)<a\\ \mathrm{Sample\; Point}& \&equals;& \left[d=2\&comma;c=5\&comma;b=26\&comma;a=7\right]\\ \mathrm{Index}& \&equals;& \left[7\&comma;13\&comma;11\&comma;9\right]\end{array}\right.$

GetFullDescription(cell);

$1<d\wedge d^2<c\wedge c^2<b\wedge \mathrm{RootOf}\left({\mathrm{\_Z}}^2-b\&comma;\mathrm{index}={\mathrm{real}}_2\right)<a$

GetSamplePoint(cell);

$\left[d=2\&comma;c=5\&comma;b=26\&comma;a=7\right]$

SignOfPolynomialOnCell( C, c-a, cell );

$\mathrm{-1}$

SignOfPolynomialOnCell( C, d-1, cell );

$1$