RegularChains[SemiAlgebraicSetTools] - Maple Programming Help

Online Help

All Products    Maple    MapleSim


Home : Support : Online Help : Mathematics : Factorization and Solving Equations : RegularChains : SemiAlgebraicSetTools Subpackage : RegularChains/SemiAlgebraicSetTools/QuantifierElimination

RegularChains[SemiAlgebraicSetTools]

  

QuantifierElimination

  

returns an equivalent formula free of quantifiers

 

Calling Sequence

Parameters

Description

Examples

References

Compatibility

Calling Sequence

QuantifierElimination(f, R, opts)

Parameters

f

-

a quantified logic formula

R

-

(optional) polynomial ring

opts

-

(optional) one or more options of the form output = rootof (literally) or simplification = simpval (where simpval is one of: false, L1, L2, L3, L4)

Description

• 

The command QuantifierElimination(f) returns a quantifier-free logic formula  qff logically equivalent to f.

• 

The user interface of Quantifier Elimination relies on the features of the Logic package. In addition to those features, we denote by &E the existential quantifier  and by &A the universal quantifier .

• 

Extended Tarski formulas are supported with the option output=rootof.

• 

The output formulas can be simplified using different levels of heuristical optimizations, from the lower-level simplification = L1 to the higher-level simplification = L4.

Examples

withRegularChains:

withSemiAlgebraicSetTools:

Suppose that we would like to solve the following Quantifier Elimination (QE) problem (due to Davenport and Heintz): find a logic formula involving d only and which is logically equivalent to the following formula

cb,aa=db=ca=cb=1a2=b

We first define a logic formula:

f&Ec,&Ab,a,a=d&andb=c&ora=c&andb=1&impliesa2=b

f&Ec,&Ab,a,a=d&andb=c&ora=c&andb=1&impliesa2=b

(1)

Then we invoke the QuantifierElimination command on the above formula

outQuantifierEliminationf

outd1=0&ord+1=0

(2)

Note that in the previous example, no variable order is specified.  In such case, the QuantifierElimination command will try to find the best elimination order according to some heuristical strategy. Alternatively, one can specify a variable order by using the PolynomialRing command as follows.

RPolynomialRingx,a,b,c

Rpolynomial_ring

(3)

On this second example below, the command QuantifierElimination(f, R) computes necessary and sufficient conditions on a, b, c for the equation to have solutions in x.

f&Ex,ax2+bx+c=0

f&Ex,ax2+bx+c=0

(4)

outQuantifierEliminationf,R

out&orc=0&comma;&andc<0&comma;b<0&comma;a=0&comma;&andc<0&comma;b<0&comma;0<a&comma;&andc<0&comma;b<0&comma;4acb2=0&comma;&andc<0&comma;b<0&comma;a<0&comma;4acb2<0&comma;&andc<0&comma;b=0&comma;0<a&comma;&andc<0&comma;0<b&comma;a=0&comma;&andc<0&comma;0<b&comma;0<a&comma;&andc<0&comma;0<b&comma;4acb2=0&comma;&andc<0&comma;0<b&comma;a<0&comma;4acb2<0&comma;&and0<c&comma;b<0&comma;a<0&comma;&and0<c&comma;b<0&comma;a=0&comma;&and0<c&comma;b<0&comma;4acb2=0&comma;&and0<c&comma;b<0&comma;0<a&comma;4acb2<0&comma;&and0<c&comma;b=0&comma;a<0&comma;&and0<c&comma;0<b&comma;a<0&comma;&and0<c&comma;0<b&comma;a=0&comma;&and0<c&comma;0<b&comma;4acb2=0&comma;&and0<c&comma;0<b&comma;0<a&comma;4acb2<0

(5)

By default, QuantifierElimination returns the standard quantifier-free formula, namely the Tarski formula. Extended Tarski formulas are supported by the option output=rootof.

f&Ex,ax2+bx+c=0

f&Ex,x2a+xb+c=0

(6)

outQuantifierEliminationf&comma;output=rootof

out&ora<0&andb24ac&comma;a=0&andb0&comma;&anda=0&comma;b=0&comma;c=0&comma;0<a&andcb24a

(7)

f&Ey,y2+x2=2

f&Ey,x2+y2=2

(8)

outQuantifierEliminationf&comma;output=rootof

out2x&andx2

(9)

f&Ey,y4+x4=2

f&Ey,x4+y4=2

(10)

outQuantifierEliminationf&comma;output=rootof

outRootOf_Z42&comma;index=real1x&andxRootOf_Z42&comma;index=real2

(11)

The output formula can be simplified optionally as follows

ff&Ei&comma;j,0i&andin&and0j&andjn&andt=nj&andp=i+j

ff&Ei&comma;j,0i&andin&and0j&andjn&andt=nj&andp=i+j

(12)

RPolynomialRingi&comma;j&comma;p&comma;t&comma;n

Rpolynomial_ring

(13)

solsQuantifierEliminationff&comma;R&comma;output=rootof&comma;simplification=false

sols&or&andn=0&comma;t=n&comma;p=0&comma;&and0<n&comma;t=0&comma;p=n&comma;&and0<n&comma;t=0&comma;n<p&comma;p<2n&comma;&and0<n&comma;t=0&comma;p=2n&comma;&and0<n&comma;0<t&comma;t<n&comma;p=t+n&comma;&and0<n&comma;0<t&comma;t<n&comma;t+n<p&comma;p<t+2n&comma;&and0<n&comma;0<t&comma;t<n&comma;p=t+2n&comma;&and0<n&comma;t=n&comma;p=0&comma;&and0<n&comma;t=n&comma;0<p&comma;p<n&comma;&and0<n&comma;t=n&comma;p=n

(14)

solsQuantifierEliminationff&comma;R&comma;output=rootof&comma;simplification=L4

sols&and0n&comma;0t&comma;tn&comma;ntp&comma;pt+2n

(15)

References

  

Changbo Chen, Marc Moreno Maza "An Incremental Algorithm for Computing Cylindrical Algebraic Decomposition." Proceedings of ASCM 2012, Computer Mathematics, Springer, (2014): 199-221.

  

Changbo Chen, Marc Moreno Maza "Quantifier elimination by cylindrical algebraic decomposition based on regular chain." J. Symb. Comput. 75: 74-93 (2016)

  

Changbo Chen, Marc Moreno Maza "Simplification of Cylindrical Algebraic Formula." Computer Algebra in Scientific Computing (CASC), Lecture Notes in Computer Science - 9301, (2015): 119-134.

Compatibility

• 

The RegularChains[SemiAlgebraicSetTools][QuantifierElimination] command was introduced in Maple 2020.

• 

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

See Also

ComprehensiveTriangularize

CylindricalDecompose

PartialCylindricalAlgebraicDecomposition

RealComprehensiveTriangularize

RealRootClassification

RealTriangularize

RegularChains

SamplePoints

Triangularize