PartialCylindricalAlgebraicDecompose - Maple Help

QuantifierElimination

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

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.

Description

 • Performs Quantifier Elimination (QE) on the input $\mathrm{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

 > $\mathrm{with}\left(\mathrm{QuantifierElimination}\right):$

Use PartialCylindricalAlgebraicDecompose for QE:

 > $\mathrm{PartialCylindricalAlgebraicDecompose}\left(\mathrm{exists}\left(x,a{x}^{2}+bx+c=0\right)\right)$
 $\left({c}{<}{0}{\wedge }{b}{<}{0}{\wedge }{a}{=}\frac{{{b}}^{{2}}}{{4}{}{c}}\right){\vee }\left({c}{<}{0}{\wedge }{b}{<}{0}{\wedge }\frac{{{b}}^{{2}}}{{4}{}{c}}{<}{a}{\wedge }{a}{<}{0}\right){\vee }\left({c}{<}{0}{\wedge }{b}{<}{0}{\wedge }{a}{=}{0}\right){\vee }\left({c}{<}{0}{\wedge }{b}{<}{0}{\wedge }{0}{<}{a}\right){\vee }\left({c}{<}{0}{\wedge }{b}{=}{0}{\wedge }{0}{<}{a}\right){\vee }\left({c}{<}{0}{\wedge }{0}{<}{b}{\wedge }{a}{=}\frac{{{b}}^{{2}}}{{4}{}{c}}\right){\vee }\left({c}{<}{0}{\wedge }{0}{<}{b}{\wedge }\frac{{{b}}^{{2}}}{{4}{}{c}}{<}{a}{\wedge }{a}{<}{0}\right){\vee }\left({c}{<}{0}{\wedge }{0}{<}{b}{\wedge }{a}{=}{0}\right){\vee }\left({c}{<}{0}{\wedge }{0}{<}{b}{\wedge }{0}{<}{a}\right){\vee }\left({c}{=}{0}{\wedge }{b}{<}{0}{\wedge }{a}{<}{0}\right){\vee }\left({c}{=}{0}{\wedge }{b}{<}{0}{\wedge }{a}{=}{0}\right){\vee }\left({c}{=}{0}{\wedge }{b}{<}{0}{\wedge }{0}{<}{a}\right){\vee }\left({c}{=}{0}{\wedge }{b}{=}{0}{\wedge }{a}{=}{0}\right){\vee }\left({c}{=}{0}{\wedge }{b}{=}{0}{\wedge }{a}{<}{0}\right){\vee }\left({c}{=}{0}{\wedge }{b}{=}{0}{\wedge }{0}{<}{a}\right){\vee }\left({c}{=}{0}{\wedge }{0}{<}{b}{\wedge }{a}{<}{0}\right){\vee }\left({c}{=}{0}{\wedge }{0}{<}{b}{\wedge }{a}{=}{0}\right){\vee }\left({c}{=}{0}{\wedge }{0}{<}{b}{\wedge }{0}{<}{a}\right){\vee }\left({0}{<}{c}{\wedge }{b}{<}{0}{\wedge }{a}{<}{0}\right){\vee }\left({0}{<}{c}{\wedge }{b}{<}{0}{\wedge }{a}{=}{0}\right){\vee }\left({0}{<}{c}{\wedge }{b}{<}{0}{\wedge }{0}{<}{a}{\wedge }{a}{<}\frac{{{b}}^{{2}}}{{4}{}{c}}\right){\vee }\left({0}{<}{c}{\wedge }{b}{<}{0}{\wedge }{a}{=}\frac{{{b}}^{{2}}}{{4}{}{c}}\right){\vee }\left({0}{<}{c}{\wedge }{b}{=}{0}{\wedge }{a}{<}{0}\right){\vee }\left({0}{<}{c}{\wedge }{0}{<}{b}{\wedge }{a}{<}{0}\right){\vee }\left({0}{<}{c}{\wedge }{0}{<}{b}{\wedge }{a}{=}{0}\right){\vee }\left({0}{<}{c}{\wedge }{0}{<}{b}{\wedge }{0}{<}{a}{\wedge }{a}{<}\frac{{{b}}^{{2}}}{{4}{}{c}}\right){\vee }\left({0}{<}{c}{\wedge }{0}{<}{b}{\wedge }{a}{=}\frac{{{b}}^{{2}}}{{4}{}{c}}\right)$ (1)

Use PartialCylindricalAlgebraicDecompose for construction of a "stock" CAD:

 > $A≔0
 ${A}{≔}{0}{<}{a}{}{{x}}^{{2}}{+}{b}{}{x}{+}{c}$ (2)
 > $C≔\mathrm{PartialCylindricalAlgebraicDecompose}\left(A,'\mathrm{output}'=\left['\mathrm{data}'\right]\right)$
 ${C}{≔}{\mathrm{CADData for set of polynomials in \left\{x, c, b, a\right\}}}$ (3)
 > $\mathrm{cells}≔{\mathrm{GetLeafCells}\left(C\right)}_{1..5}$
 ${\mathrm{cells}}{≔}\left[{\mathrm{Level 4 CADCell with local description a < -\left(b*x+c\right)/x^2 and local sample point a = -2}}{,}{\mathrm{Level 4 CADCell with local description a = -\left(b*x+c\right)/x^2 and local sample point a = -1}}{,}{\mathrm{Level 4 CADCell with local description -\left(b*x+c\right)/x^2 < a and local sample point a = 0}}{,}{\mathrm{Level 4 CADCell with local description a < -\left(b*x+c\right)/x^2 and local sample point a = -1}}{,}{\mathrm{Level 4 CADCell with local description a = -\left(b*x+c\right)/x^2 and local sample point a = 0}}\right]$ (4)
 > $\mathrm{GetFullDescription}\left({\mathrm{cells}}_{1}\right)$
 ${x}{<}{0}{\wedge }{c}{<}{0}{\wedge }{b}{<}{-}\frac{{c}}{{x}}{\wedge }{a}{<}{-}\frac{{b}{}{x}{+}{c}}{{{x}}^{{2}}}$ (5)

Compatibility

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