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

Online Help

All Products    Maple    MapleSim


QuantifierElimination

  

PartialCylindricalAlgebraicDecompose

  

compute a partial cylindrical algebraic decomposition on a real polynomial formula, usually for quantifier elimination

 

Calling Sequence

Parameters

Returns

Description

Examples

Compatibility

Calling Sequence

PartialCylindricalAlgebraicDecompose( phi, cadqeopts )

PartialCylindricalAlgebraicDecompose( F, cadcoreopts )

Parameters

phi

-

a quantified rational Tarski formula

F

-

an unquantified rational Tarski formula

cadqeopts

-

keyword options relevant to QE by CAD, and/or core keyword options for CAD

cadcoreopts

-

core keyword options for cylindrical algebraic decomposition

Returns

• 

When phi is passed, up to three outputs depending on the value of the keyword option output, described in QuantifierElimination options.

• 

When F is passed, a CADData object containing the data structures used in CAD, which can be inspected via various CADData methods.

• 

See QuantifierElimination options for information on cadqeopts and cadcoreopts.

Description

• 

Performs Quantifier Elimination (QE) on the input expr purely by the Cylindrical Algebraic Decomposition (CAD) method, as opposed to QuantifierEliminate which will use Virtual Term Substitution (VTS) as far as possible before using CAD.

• 

This function uses Partial CAD, which aims to terminate building the CAD as soon as an answer can be deduced. Using a low eagerness value forces building the whole CAD without early termination.

• 

The input need not be in prenex form, however it is converted to prenex form right away for the purposes of computation.

• 

Information on keyword options for the routine can be found in the help page QuantifierElimination options.

Examples

withQuantifierElimination:

Use PartialCylindricalAlgebraicDecompose for QE:

PartialCylindricalAlgebraicDecomposeexistsx,ax2+bx+c=0

c<0b<0a=b24cc<0b<0b24c<aa<0c<0b<0a=0c<0b<00<ac<0b=00<ac<00<ba=b24cc<00<bb24c<aa<0c<00<ba=0c<00<b0<ac=0b<0a<0c=0b<0a=0c=0b<00<ac=0b=0a=0c=0b=0a<0c=0b=00<ac=00<ba<0c=00<ba=0c=00<b0<a0<cb<0a<00<cb<0a=00<cb<00<aa<b24c0<cb<0a=b24c0<cb=0a<00<c0<ba<00<c0<ba=00<c0<b0<aa<b24c0<c0<ba=b24c

(1)

Use PartialCylindricalAlgebraicDecompose for construction of a "stock" CAD:

A0<ax2&plus;bx&plus;c

A0<ax2+bx+c

(2)

CPartialCylindricalAlgebraicDecomposeA&comma;&apos;output&apos;&equals;&apos;data&apos;

CCADData for set of polynomials in {x, c, b, a}

(3)

cellsGetLeafCellsC1..5

cellsLevel 4 CADCell with local description a < -(b*x+c)/x^2 and local sample point a = -2&comma;Level 4 CADCell with local description a = -(b*x+c)/x^2 and local sample point a = -1&comma;Level 4 CADCell with local description -(b*x+c)/x^2 < a and local sample point a = 0&comma;Level 4 CADCell with local description a < -(b*x+c)/x^2 and local sample point a = -1&comma;Level 4 CADCell with local description a = -(b*x+c)/x^2 and local sample point a = 0

(4)

GetFullDescriptioncells1

x<0c<0b<cxa<bx+cx2

(5)

Compatibility

• 

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

• 

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

See Also

CylindricalAlgebraicDecompose

QuantifierEliminate

QuantifierElimination

QuantifierElimination options