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

Online Help

All Products    Maple    MapleSim


QuantifierElimination

  

QuantifierEliminate

  

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

 

Calling Sequence

Parameters

Returns

Description

Examples

Compatibility

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

withQuantifierElimination:

QuantifierEliminateexistsx&comma;y&comma;z&comma;0<xyz

true

(1)

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

qf&comma;wQuantifierEliminateexistsx&comma;y&comma;z&comma;0<xyz&comma;&apos;mode&equals;breadth&apos;&comma;&apos;eagerness&apos;&equals;1&comma;&apos;output&equals;qf&comma;witnesses&apos;

qf,wtrue,true&comma;z=12&comma;y=12&comma;x=12&comma;true&comma;z=12&comma;y=12&comma;x=12&comma;true&comma;z=12&comma;y=−2&comma;x=−2&comma;true&comma;z=−2&comma;y=12&comma;x=−2&comma;true&comma;z=−2&comma;y=−2&comma;x=12&comma;true&comma;z=12&comma;y=12&comma;x=12&comma;true&comma;z=12&comma;y=−2&comma;x=−2&comma;true&comma;z=12&comma;y=12&comma;x=12&comma;true&comma;z=−2&comma;y=12&comma;x=−2

(2)

exprexistsx&comma;forally&comma;existsz&comma;And4x2&plus;xy2z&plus;14&equals;0&comma;2x&plus;y2z&plus;12&equals;0&comma;x2z1x2y2&equals;0

exprx&comma;y&comma;z&comma;4x2+xy2z+14=02x+y2z+12=0x2z12xy2=0

(3)

QuantifierEliminateexpr

false

(4)

QuantifierEliminateforallx&comma;Implies0<x&comma;0<x2

true

(5)

QuantifierEliminateforallx&comma;Implies0x&comma;0<x2

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:

exprexistsv1&comma;v2&comma;v3&comma;v4&comma;v5&comma;v6&comma;v7&comma;v8&comma;Andv7<0&comma;0<v8&comma;0<v4&comma;v2v6&plus;v3v8&equals;v4&comma;v1v5&plus;v3v7&equals;v4&comma;v6&equals;1&comma;v5&equals;1&comma;0<v1

exprv1&comma;v2&comma;v3&comma;v4&comma;v5&comma;v6&comma;v7&comma;v8&comma;v7<00<v80<v4v2v6+v3v8=v4v1v5+v3v7=v4v6=1v5=10<v1

(7)

qf&comma;w&comma;dataQuantifierEliminateexpr&comma;&apos;output&apos;&equals;&apos;qf&apos;&comma;&apos;witnesses&apos;&comma;&apos;data&apos;

qf,w,datatrue,true&comma;v8=92&comma;v7=12&comma;v6=1&comma;v5=1&comma;v4=14&comma;v3=12&comma;v2=−2&comma;v1=12,QEData forv1&comma;v2&comma;v3&comma;v4&comma;v5&comma;v6&comma;v7&comma;v8&comma;v7<0v8<0v4<0v2v6+v3v8v4=0v1v5+v3v7v4=0v61=0v51=0v1<0

(8)

Compatibility

• 

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

• 

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

See Also

DeleteFormula

InsertFormula

PartialCylindricalAlgebraicDecompose

QuantifierElimination

QuantifierElimination options