 Quantifier Elimination - Maple Help

Home : Support : Online Help : What's New and Release Notes : Quantifier Elimination

Quantifier Elimination in Maple 2023 Description

 • 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]$ (1)
 > 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}{,}{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)$ (2)
 > QuantifierEliminate(expr);
 ${\mathrm{false}}$ (3)
 • 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}{,}\mathrm{v__2}{,}\mathrm{v__3}{,}\mathrm{v__4}{,}\mathrm{v__5}{,}\mathrm{v__6}{,}\mathrm{v__7}{,}\mathrm{v__8}\right]{,}\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)$ (4)
 > (qf, witnesses) := QuantifierEliminate( expr, 'output = [ qf, witnesses]' );
 ${\mathrm{qf}}{,}{\mathrm{witnesses}}{≔}{\mathrm{true}}{,}\left[\left[{\mathrm{true}}{,}\mathrm{v__8}{=}\frac{{9}}{{2}}{,}\mathrm{v__7}{=}{-}\frac{{1}}{{2}}{,}\mathrm{v__6}{=}{1}{,}\mathrm{v__5}{=}{1}{,}\mathrm{v__4}{=}\frac{{1}}{{4}}{,}\mathrm{v__3}{=}\frac{{1}}{{2}}{,}\mathrm{v__2}{=}{-2}{,}\mathrm{v__1}{=}\frac{{1}}{{2}}\right]\right]$ (5)
 > map(evalb,eval(op(2,expr),witnesses[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}}$ (6)
 • 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}{,}{\forall }{}\left(\left[{b}{,}{a}\right]{,}\left({a}{-}{d}{=}{0}{\wedge }{b}{-}{c}{=}{0}\right){\vee }\left({a}{-}{c}{=}{0}{\wedge }{b}{-}{1}{=}{0}\right){⇒}{{a}}^{{2}}{-}{b}{=}{0}\right)\right)$ (7)
 > PartialCylindricalAlgebraicDecompose(expr);
 ${d}{=}{-1}{\vee }{d}{=}{1}$ (8)
 • QuantifierTools is a subpackage of QuantifierElimination that offers tools for working with and manipulating Tarski formulae:
 > with(QuantifierTools);
 $\left[{\mathrm{AlphaConvert}}{,}{\mathrm{ConvertRationalConstraintsToTarski}}{,}{\mathrm{ConvertToPrenexForm}}{,}{\mathrm{GetAllPolynomials}}{,}{\mathrm{GetEquationalConstraints}}{,}{\mathrm{GetUnquantifiedFormula}}{,}{\mathrm{NegateFormula}}{,}{\mathrm{SuggestCADOptions}}\right]$ (9)
 > uqf := GetUnquantifiedFormula( expr );
 ${\mathrm{uqf}}{≔}\left({a}{-}{d}{=}{0}{\wedge }{b}{-}{c}{=}{0}\right){\vee }\left({a}{-}{c}{=}{0}{\wedge }{b}{-}{1}{=}{0}\right){⇒}{{a}}^{{2}}{-}{b}{=}{0}$ (10)
 • 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}{≔}{\mathrm{CADData for set of polynomials in \left\{d, c, b, a\right\}}}$ (11)
 > leaves := GetLeafCells( C )[ 1 .. 5 ];
 ${\mathrm{leaves}}{≔}\left[{\mathrm{Level 4 CADCell with local description RootOf\left(_Z^2-b,index = real\left[2\right]\right) < a and local sample point a = 7}}{,}{\mathrm{Level 4 CADCell with local description a = RootOf\left(_Z^2-b,index = real\left[2\right]\right) and local sample point a = RootOf\left(_Z^2-26,48158877692977696785785/9444732965739290427392 .. 24079438846488848392933/4722366482869645213696\right)}}{,}{\mathrm{Level 4 CADCell with local description And\left(c < a,a < RootOf\left(_Z^2-b,index = real\left[2\right]\right)\right) and local sample point a = 61/12}}{,}{\mathrm{Level 4 CADCell with local description a = c and local sample point a = 5}}{,}{\mathrm{Level 4 CADCell with local description And\left(d < a,a < c\right) and local sample point a = 3}}\right]$ (12)
 > cell := leaves;
 ${\mathrm{cell}}{≔}{\mathrm{Level 4 CADCell with local description RootOf\left(_Z^2-b,index = real\left[2\right]\right) < a and local sample point a = 7}}$ (13)
 > GetFullDescription(cell);
 ${1}{<}{d}{\wedge }{{d}}^{{2}}{<}{c}{\wedge }{{c}}^{{2}}{<}{b}{\wedge }{\mathrm{RootOf}}{}\left({{\mathrm{_Z}}}^{{2}}{-}{b}{,}{\mathrm{index}}{=}{{\mathrm{real}}}_{{2}}\right){<}{a}$ (14)
 > GetSamplePoint(cell);
 $\left[{d}{=}{2}{,}{c}{=}{5}{,}{b}{=}{26}{,}{a}{=}{7}\right]$ (15)
 > SignOfPolynomialOnCell( C, c-a, cell );
 ${-1}$ (16)
 > SignOfPolynomialOnCell( C, d-1, cell );
 ${1}$ (17)