QuantifierElimination
PartialCylindricalAlgebraicDecompose
compute a partial cylindrical algebraic decomposition on a real polynomial formula, usually for quantifier elimination
Calling Sequence
Parameters
Returns
Description
Examples
Compatibility
PartialCylindricalAlgebraicDecompose( phi, cadqeopts )
PartialCylindricalAlgebraicDecompose( F, cadcoreopts )
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
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.
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.
withQuantifierElimination:
Use PartialCylindricalAlgebraicDecompose for QE:
PartialCylindricalAlgebraicDecomposeexistsx,ax2+bx+c=0
c<0∧b<0∧a=b24c∨c<0∧b<0∧b24c<a∧a<0∨c<0∧b<0∧a=0∨c<0∧b<0∧0<a∨c<0∧b=0∧0<a∨c<0∧0<b∧a=b24c∨c<0∧0<b∧b24c<a∧a<0∨c<0∧0<b∧a=0∨c<0∧0<b∧0<a∨c=0∧b<0∧a<0∨c=0∧b<0∧a=0∨c=0∧b<0∧0<a∨c=0∧b=0∧a=0∨c=0∧b=0∧a<0∨c=0∧b=0∧0<a∨c=0∧0<b∧a<0∨c=0∧0<b∧a=0∨c=0∧0<b∧0<a∨0<c∧b<0∧a<0∨0<c∧b<0∧a=0∨0<c∧b<0∧0<a∧a<b24c∨0<c∧b<0∧a=b24c∨0<c∧b=0∧a<0∨0<c∧0<b∧a<0∨0<c∧0<b∧a=0∨0<c∧0<b∧0<a∧a<b24c∨0<c∧0<b∧a=b24c
Use PartialCylindricalAlgebraicDecompose for construction of a "stock" CAD:
A≔0<ax2+bx+c
C≔PartialCylindricalAlgebraicDecomposeA,output=data
C≔Variables=x,c,b,aInput Polynomials=cxbx+cax2+bx+c# Cells=57Projection polynomials for level 1=xProjection polynomials for level 2=cProjection polynomials for level 3=bx+cProjection polynomials for level 4=ax2+bx+c
cells≔GetCellsC1..5
cells≔Description=x<0∧c<0∧b<−cx∧a<−bx+cx2Sample Point=x=−1,c=−1,b=−2,a=−2Index=1,1,1,1,Description=x<0∧c<0∧b<−cx∧a=−bx+cx2Sample Point=x=−1,c=−1,b=−2,a=−1Index=1,1,1,2,Description=x<0∧c<0∧b<−cx∧−bx+cx2<aSample Point=x=−1,c=−1,b=−2,a=0Index=1,1,1,3,Description=x<0∧c<0∧b=−cx∧a<0Sample Point=x=−1,c=−1,b=−1,a=−1Index=1,1,2,1,Description=x<0∧c<0∧b=−cx∧a=0Sample Point=x=−1,c=−1,b=−1,a=0Index=1,1,2,2
GetFullDescriptioncells1
x<0∧c<0∧b<−cx∧a<−bx+cx2
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 options
Download Help Document
