Overview of the QuantifierElimination Package
Description
List of QuantifierElimination Commands
List of QuantifierElimination Subpackages
Examples
References
Compatibility
The QuantifierElimination package contains routines for quantifier elimination (QE) over the reals, as well as other related auxiliary tools for working with Tarski formulae and other related formulae.
QuantifierEliminate, PartialCylindricalAlgebraicDecompose, InsertFormula, and DeleteFormula are all routines to perform QE. The latter two routines are "evolutionary" methods [Ton19], which is a term usually referred to in other academic literature as "incremental".
CylindricalAlgebraicDecompose is a routine to produce "stock" Cylindrical Algebraic Decompositions (CADs) for sets of polynomials or formulae. CADs have many uses in real algebraic geometry.
PartialCylindricalAlgebraicDecompose can also be used for such purposes, where partial CAD is used to attempt to construct minimal geometry depending on truth values. Generally, PartialCylindricalAlgebraicDecompose is a quantifier elimination tool in the same manner as QuantifierEliminate. Where CAD is used for the purposes of quantifier elimination, the methodology is partial CAD [CH91] for lifting to aim for early termination.
QuantifierEliminate, InsertFormula, and DeleteFormula use poly-algorithmic methodology for quantifier elimination between two prolific algorithms for QE, Virtual Term Substitution (VTS) and Cylindrical Algebraic Decomposition (CAD) [Ton20].
Where VTS is implemented, the main sources of algorithms is [Kos16]. VTS is an algorithm best suited to elimination of quantified variables appearing at low degree in the input formula. VTS within QuantifierElimination is implemented to eliminate variables appearing up to quadratically in a formula, pending factorization of polynomials.
Where quantifier elimination is offered by the package, routines follow an output syntax defined by a keyword option output. This option enables production of the quantifier-free answer for a QE problem, as well as "witnesses" that prove equivalence of QE to a quantifier-free answer. Additionally, requesting data provides QEData or CADData objects that enable QE in an incremental fashion, along with other methods to enable inspection of the data structures in greater detail. For more information, see the help page QuantifierElimination options.
Witnesses can be requested for any QE formula that is fully quantified with only one type of quantifier symbol (forall or exists). Production of witnesses is possible under any methodology within QuantifierElimination, including poly-algorithmic or pure CAD. Production of witnesses from VTS is discussed in [Ton20, KS16].
The methodology for production of CADs within QuantifierElimination is always projection and lifting, where the projection operator implemented is the Lazard projection operator [Laz94, MPP19].
The QuantifierTools subpackage is a source of auxiliary tools for working with formulae and other outputs from QuantifierElimination.
Where equational constraints are used within CAD in the package, curtain occurrences may prevent the output from being mathematically correct. The package implements algorithms to try to recover from such occurrences to maximize the chance of success [NDS19, Ton21].
The package uses a number of keyword options that are common across routines for the package, especially those offering quantifier elimination. These options are dependent and specific to the methodology used within the routine on request.
The work [Ton21] is the main academic source of reference for the package.
QuantifierEliminate
QuantifierElimination:-CylindricalAlgebraicDecompose
QuantifierElimination:-DeleteFormula
QuantifierElimination:-InsertFormula
QuantifierElimination:-PartialCylindricalAlgebraicDecompose
QuantifierTools
withQuantifierElimination
CylindricalAlgebraicDecompose,DeleteFormula,InsertFormula,PartialCylindricalAlgebraicDecompose,QuantifierEliminate,QuantifierTools
QuantifierEliminateexistsx,ax2+bx+c=0
a=0∧b=0∧c=0∨a=0∧b≠0∧ac2=0∨a<0∧4ac−b2<0∨a≠0∧4ac−b2≤0∨−a<0∧4ac−b2<0
PartialCylindricalAlgebraicDecomposeexistsx,ax3+bx2+cx+d=0
d<0∧c<0∧b<c23d∧a<0∨d<0∧c<0∧b<c23d∧0<a∨d<0∧c<0∧b=c23d∧a<RootOf729d4_Z2−54c3_Zd2+c6,index=real1∨d<0∧c<0∧b=c23d∧a=RootOf729d4_Z2−54c3_Zd2+c6,index=real1∨d<0∧c<0∧b=c23d∧RootOf729d4_Z2−54c3_Zd2+c6,index=real1<a∧a<0∨d<0∧c<0∧b=c23d∧0<a∨d<0∧c<0∧c23d<b∧b<c24d∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨d<0∧c<0∧c23d<b∧b<c24d∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨d<0∧c<0∧c23d<b∧b<c24d∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1<a∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨d<0∧c<0∧c23d<b∧b<c24d∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨d<0∧c<0∧c23d<b∧b<c24d∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2<a∧a<0∨d<0∧c<0∧c23d<b∧b<c24d∧0<a∨d<0∧c<0∧b=c24d∧a<RootOf_Z54d2_Z−c3,index=real1∨d<0∧c<0∧b=c24d∧a=RootOf_Z54d2_Z−c3,index=real1∨d<0∧c<0∧b=c24d∧RootOf_Z54d2_Z−c3,index=real1<a∧a<RootOf_Z54d2_Z−c3,index=real2∨d<0∧c<0∧b=c24d∧a=RootOf_Z54d2_Z−c3,index=real2∨d<0∧c<0∧b=c24d∧RootOf_Z54d2_Z−c3,index=real2<a∨d<0∧c<0∧c24d<b∧b<0∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨d<0∧c<0∧c24d<b∧b<0∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨d<0∧c<0∧c24d<b∧b<0∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1<a∧a<0∨d<0∧c<0∧c24d<b∧b<0∧a=0∨d<0∧c<0∧c24d<b∧b<0∧0<a∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨d<0∧c<0∧c24d<b∧b<0∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨d<0∧c<0∧c24d<b∧b<0∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2<a∨d<0∧c<0∧b=0∧a<RootOf_Z27d2_Z+4c3,index=real1∨d<0∧c<0∧b=0∧a=RootOf_Z27d2_Z+4c3,index=real1∨d<0∧c<0∧b=0∧RootOf_Z27d2_Z+4c3,index=real1<a∧a<RootOf_Z27d2_Z+4c3,index=real2∨d<0∧c<0∧b=0∧a=RootOf_Z27d2_Z+4c3,index=real2∨d<0∧c<0∧b=0∧RootOf_Z27d2_Z+4c3,index=real2<a∨d<0∧c<0∧0<b∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨d<0∧c<0∧0<b∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨d<0∧c<0∧0<b∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1<a∧a<0∨d<0∧c<0∧0<b∧a=0∨d<0∧c<0∧0<b∧0<a∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨d<0∧c<0∧0<b∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨d<0∧c<0∧0<b∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2<a∨d<0∧c=0∧b<0∧a<0∨d<0∧c=0∧b<0∧0<a∨d<0∧c=0∧b=0∧a<0∨d<0∧c=0∧b=0∧0<a∨d<0∧c=0∧0<b∧a<RootOf27_Z2d+4b3,index=real1∨d<0∧c=0∧0<b∧a=RootOf27_Z2d+4b3,index=real1∨d<0∧c=0∧0<b∧RootOf27_Z2d+4b3,index=real1<a∧a<0∨d<0∧c=0∧0<b∧a=0∨d<0∧c=0∧0<b∧0<a∧a<RootOf27_Z2d+4b3,index=real2∨d<0∧c=0∧0<b∧a=RootOf27_Z2d+4b3,index=real2∨d<0∧c=0∧0<b∧RootOf27_Z2d+4b3,index=real2<a∨d<0∧0<c∧b<c23d∧a<0∨d<0∧0<c∧b<c23d∧0<a∨d<0∧0<c∧b=c23d∧a<0∨d<0∧0<c∧b=c23d∧0<a∧a<RootOf729d4_Z2−54c3_Zd2+c6,index=real1∨d<0∧0<c∧b=c23d∧a=RootOf729d4_Z2−54c3_Zd2+c6,index=real1∨d<0∧0<c∧b=c23d∧RootOf729d4_Z2−54c3_Zd2+c6,index=real1<a∨d<0∧0<c∧c23d<b∧b<c24d∧a<0∨d<0∧0<c∧c23d<b∧b<c24d∧0<a∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨d<0∧0<c∧c23d<b∧b<c24d∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨d<0∧0<c∧c23d<b∧b<c24d∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1<a∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨d<0∧0<c∧c23d<b∧b<c24d∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨d<0∧0<c∧c23d<b∧b<c24d∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2<a∨d<0∧0<c∧b=c24d∧a<RootOf_Z54d2_Z−c3,index=real1∨d<0∧0<c∧b=c24d∧a=RootOf_Z54d2_Z−c3,index=real1∨d<0∧0<c∧b=c24d∧RootOf_Z54d2_Z−c3,index=real1<a∧a<RootOf_Z54d2_Z−c3,index=real2∨d<0∧0<c∧b=c24d∧a=RootOf_Z54d2_Z−c3,index=real2∨d<0∧0<c∧b=c24d∧RootOf_Z54d2_Z−c3,index=real2<a∨d<0∧0<c∧c24d<b∧b<0∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨d<0∧0<c∧c24d<b∧b<0∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨d<0∧0<c∧c24d<b∧b<0∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1<a∧a<0∨d<0∧0<c∧c24d<b∧b<0∧a=0∨d<0∧0<c∧c24d<b∧b<0∧0<a∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨d<0∧0<c∧c24d<b∧b<0∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨d<0∧0<c∧c24d<b∧b<0∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2<a∨d<0∧0<c∧b=0∧a<RootOf_Z27d2_Z+4c3,index=real1∨d<0∧0<c∧b=0∧a=RootOf_Z27d2_Z+4c3,index=real1∨d<0∧0<c∧b=0∧RootOf_Z27d2_Z+4c3,index=real1<a∧a<RootOf_Z27d2_Z+4c3,index=real2∨d<0∧0<c∧b=0∧a=RootOf_Z27d2_Z+4c3,index=real2∨d<0∧0<c∧b=0∧RootOf_Z27d2_Z+4c3,index=real2<a∨d<0∧0<c∧0<b∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨d<0∧0<c∧0<b∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨d<0∧0<c∧0<b∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1<a∧a<0∨d<0∧0<c∧0<b∧a=0∨d<0∧0<c∧0<b∧0<a∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨d<0∧0<c∧0<b∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨d<0∧0<c∧0<b∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2<a∨d=0∧c<0∧b<0∧a<b24c∨d=0∧c<0∧b<0∧a=b24c∨d=0∧c<0∧b<0∧b24c<a∧a<0∨d=0∧c<0∧b<0∧a=0∨d=0∧c<0∧b<0∧0<a∨d=0∧c<0∧b=0∧a<0∨d=0∧c<0∧b=0∧a=0∨d=0∧c<0∧b=0∧0<a∨d=0∧c<0∧0<b∧a<b24c∨d=0∧c<0∧0<b∧a=b24c∨d=0∧c<0∧0<b∧b24c<a∧a<0∨d=0∧c<0∧0<b∧a=0∨d=0∧c<0∧0<b∧0<a∨d=0∧c=0∧b<0∧a<0∨d=0∧c=0∧b<0∧a=0∨d=0∧c=0∧b<0∧0<a∨d=0∧c=0∧b=0∧a=0∨d=0∧c=0∧b=0∧a<0∨d=0∧c=0∧b=0∧0<a∨d=0∧c=0∧0<b∧a<0∨d=0∧c=0∧0<b∧a=0∨d=0∧c=0∧0<b∧0<a∨d=0∧0<c∧b<0∧a<0∨d=0∧0<c∧b<0∧a=0∨d=0∧0<c∧b<0∧0<a∧a<b24c∨d=0∧0<c∧b<0∧a=b24c∨d=0∧0<c∧b<0∧b24c<a∨d=0∧0<c∧b=0∧a<0∨d=0∧0<c∧b=0∧a=0∨d=0∧0<c∧b=0∧0<a∨d=0∧0<c∧0<b∧a<0∨d=0∧0<c∧0<b∧a=0∨d=0∧0<c∧0<b∧0<a∧a<b24c∨d=0∧0<c∧0<b∧a=b24c∨d=0∧0<c∧0<b∧b24c<a∨0<d∧c<0∧b<0∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨0<d∧c<0∧b<0∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨0<d∧c<0∧b<0∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1<a∧a<0∨0<d∧c<0∧b<0∧a=0∨0<d∧c<0∧b<0∧0<a∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨0<d∧c<0∧b<0∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨0<d∧c<0∧b<0∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2<a∨0<d∧c<0∧b=0∧a<RootOf_Z27d2_Z+4c3,index=real1∨0<d∧c<0∧b=0∧a=RootOf_Z27d2_Z+4c3,index=real1∨0<d∧c<0∧b=0∧RootOf_Z27d2_Z+4c3,index=real1<a∧a<RootOf_Z27d2_Z+4c3,index=real2∨0<d∧c<0∧b=0∧a=RootOf_Z27d2_Z+4c3,index=real2∨0<d∧c<0∧b=0∧RootOf_Z27d2_Z+4c3,index=real2<a∨0<d∧c<0∧0<b∧b<c24d∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨0<d∧c<0∧0<b∧b<c24d∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨0<d∧c<0∧0<b∧b<c24d∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1<a∧a<0∨0<d∧c<0∧0<b∧b<c24d∧a=0∨0<d∧c<0∧0<b∧b<c24d∧0<a∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨0<d∧c<0∧0<b∧b<c24d∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨0<d∧c<0∧0<b∧b<c24d∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2<a∨0<d∧c<0∧b=c24d∧a<RootOf_Z54d2_Z−c3,index=real1∨0<d∧c<0∧b=c24d∧a=RootOf_Z54d2_Z−c3,index=real1∨0<d∧c<0∧b=c24d∧RootOf_Z54d2_Z−c3,index=real1<a∧a<RootOf_Z54d2_Z−c3,index=real2∨0<d∧c<0∧b=c24d∧a=RootOf_Z54d2_Z−c3,index=real2∨0<d∧c<0∧b=c24d∧RootOf_Z54d2_Z−c3,index=real2<a∨0<d∧c<0∧c24d<b∧b<c23d∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨0<d∧c<0∧c24d<b∧b<c23d∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨0<d∧c<0∧c24d<b∧b<c23d∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1<a∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨0<d∧c<0∧c24d<b∧b<c23d∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨0<d∧c<0∧c24d<b∧b<c23d∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2<a∧a<0∨0<d∧c<0∧c24d<b∧b<c23d∧0<a∨0<d∧c<0∧b=c23d∧a<RootOf729d4_Z2−54c3_Zd2+c6,index=real1∨0<d∧c<0∧b=c23d∧a=RootOf729d4_Z2−54c3_Zd2+c6,index=real1∨0<d∧c<0∧b=c23d∧RootOf729d4_Z2−54c3_Zd2+c6,index=real1<a∧a<0∨0<d∧c<0∧b=c23d∧0<a∨0<d∧c<0∧c23d<b∧a<0∨0<d∧c<0∧c23d<b∧0<a∨0<d∧c=0∧b<0∧a<RootOf27_Z2d+4b3,index=real1∨0<d∧c=0∧b<0∧a=RootOf27_Z2d+4b3,index=real1∨0<d∧c=0∧b<0∧RootOf27_Z2d+4b3,index=real1<a∧a<0∨0<d∧c=0∧b<0∧a=0∨0<d∧c=0∧b<0∧0<a∧a<RootOf27_Z2d+4b3,index=real2∨0<d∧c=0∧b<0∧a=RootOf27_Z2d+4b3,index=real2∨0<d∧c=0∧b<0∧RootOf27_Z2d+4b3,index=real2<a∨0<d∧c=0∧b=0∧a<0∨0<d∧c=0∧b=0∧0<a∨0<d∧c=0∧0<b∧a<0∨0<d∧c=0∧0<b∧0<a∨0<d∧0<c∧b<0∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨0<d∧0<c∧b<0∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨0<d∧0<c∧b<0∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1<a∧a<0∨0<d∧0<c∧b<0∧a=0∨0<d∧0<c∧b<0∧0<a∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨0<d∧0<c∧b<0∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨0<d∧0<c∧b<0∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2<a∨0<d∧0<c∧b=0∧a<RootOf_Z27d2_Z+4c3,index=real1∨0<d∧0<c∧b=0∧a=RootOf_Z27d2_Z+4c3,index=real1∨0<d∧0<c∧b=0∧RootOf_Z27d2_Z+4c3,index=real1<a∧a<RootOf_Z27d2_Z+4c3,index=real2∨0<d∧0<c∧b=0∧a=RootOf_Z27d2_Z+4c3,index=real2∨0<d∧0<c∧b=0∧RootOf_Z27d2_Z+4c3,index=real2<a∨0<d∧0<c∧0<b∧b<c24d∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨0<d∧0<c∧0<b∧b<c24d∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨0<d∧0<c∧0<b∧b<c24d∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1<a∧a<0∨0<d∧0<c∧0<b∧b<c24d∧a=0∨0<d∧0<c∧0<b∧b<c24d∧0<a∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨0<d∧0<c∧0<b∧b<c24d∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨0<d∧0<c∧0<b∧b<c24d∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2<a∨0<d∧0<c∧b=c24d∧a<RootOf_Z54d2_Z−c3,index=real1∨0<d∧0<c∧b=c24d∧a=RootOf_Z54d2_Z−c3,index=real1∨0<d∧0<c∧b=c24d∧RootOf_Z54d2_Z−c3,index=real1<a∧a<RootOf_Z54d2_Z−c3,index=real2∨0<d∧0<c∧b=c24d∧a=RootOf_Z54d2_Z−c3,index=real2∨0<d∧0<c∧b=c24d∧RootOf_Z54d2_Z−c3,index=real2<a∨0<d∧0<c∧c24d<b∧b<c23d∧a<0∨0<d∧0<c∧c24d<b∧b<c23d∧0<a∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨0<d∧0<c∧c24d<b∧b<c23d∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1∨0<d∧0<c∧c24d<b∧b<c23d∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real1<a∧a<RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨0<d∧0<c∧c24d<b∧b<c23d∧a=RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2∨0<d∧0<c∧c24d<b∧b<c23d∧RootOf27d2_Z2+−18bcd+4c3_Z+4b3d−b2c2,index=real2<a∨0<d∧0<c∧b=c23d∧a<0∨0<d∧0<c∧b=c23d∧0<a∧a<RootOf729d4_Z2−54c3_Zd2+c6,index=real1∨0<d∧0<c∧b=c23d∧a=RootOf729d4_Z2−54c3_Zd2+c6,index=real1∨0<d∧0<c∧b=c23d∧RootOf729d4_Z2−54c3_Zd2+c6,index=real1<a∨0<d∧0<c∧c23d<b∧a<0∨0<d∧0<c∧c23d<b∧0<a
PartialCylindricalAlgebraicDecomposeexistsx,forally,Andx2+y2−2<0,Ory<x,x<0
false
A≔x−3RootOfx2−2,1..2,x2+y2−2
A≔x−3RootOf_Z2−2,1..2,x2+y2−2
CylindricalAlgebraicDecomposeA
Variables=y,xInput Polynomials=x−3RootOf_Z2−2,1..2y2−2y2+16x2+y2−2# Cells=23Projection polynomials for level 1=y2−2y2+16Projection polynomials for level 2=x−3RootOf_Z2−2,1..2x2+y2−2
[CH91] Hong, H. and Collins, G.E. Partial Cylindrical Algebraic Decomposition for Quantifier Elimination. Journal of Symbolic Computation, pages 299–328, 1991.
[Laz94] Lazard, D. An Improved Projection for Cylindrical Algebraic Decomposition. In Chandrajit L. Bajaj, editor, Algebraic Geometry and its Applications, pages 467–476. Springer New York, New York, NY, 1994.
[KS16] Kǒsta, M. and Sturm, T. and Dolzmann, A. Better answers to real questions. Journal of Symbolic Computation, 74:255 – 275, 5 2016.
[Kos16] Kǒsta, M. New Concepts for Real Quantifier Elimination by Virtual Substitution. PhD Thesis, Universität des Saarlandes, 2016.
[MPP19] McCallum, S. Parusinski, A. and Paunescu, L. Validity proof of Lazard's method for CAD construction. Journal of Symbolic Computation, 92:52–69, 2019.
[NDS19] Nair A.S., Davenport, J.H., and Sankaran, G. On Benefits of Equality Constraints in Lex-Least Invariant CAD. In Proceedings SC2 Workshop 2019. CEUR Workshop Proceedings, 10 2019.
[Ton19] Tonks, Z. Evolutionary Virtual Term Substitution in a Quantifier Elimination System. In Proceedings SC2 Workshop 2019. CEUR Workshop Proceedings, 10 2019.
[Ton20] Tonks, Z. A Poly-algorithmic Quantifier Elimination Package in Maple. In Jürgen Gerhard and Ilias Kotsireas, editors, Maple in Mathematics Education and Research, pages 176-186, 2020. Springer International Publishing.
[Ton21] Tonks, Z. Poly-algorithmic Techniques in Real Quantifier Elimination. PhD Thesis, University of Bath, UK, 2021.
The QuantifierElimination package was introduced in Maple 2023.
For more information on Maple 2023 changes, see Updates in Maple 2023.
See Also
Quantifier Elimination examples
Download Help Document
