Advanced Search

Question: Is there any bug in the new Quantifier Elimination package?

Question:Is there any bug in the new Quantifier Elimination package?

sursumCorda 1079 Maple 2023
quantifierelimination
April 01 2023
0

The QuantifierElimination package has been added in Maple 2023.
However, in the following example, the old (yet not obsolete) RegularChains:-SemiAlgebraicSetTools:-QuantifierElimination command can solve the problem, but strangely, the new QuantifierElimination:-QuantifierEliminate command simply returns an error. 
 

> 

restart;
> 

RegularChains:-SemiAlgebraicSetTools:-QuantifierElimination(:-`&A`([x, y, t]), :-`&implies`(:-`&and`(x^3+y^2-x = t, t^2 = 4/27, t < 0), x^2+y^2 >= rho), output = rootof)

rho <= 1/3

 (1)
> 

QuantifierElimination:-QuantifierEliminate(:-forall([x, y, t], :-Implies(:-And(x^3+y^2-x = t, t^2 = 4/27, t < 0), x^2+y^2 >= rho)))

Error, (in CADCell:-CCHILD) intervals the same at this precision

  
> 

Digits += 5:
> 

RegularChains:-SemiAlgebraicSetTools:-QuantifierElimination(:-`&A`([x, y, t]), :-`&implies`(:-`&and`(x^3+y^2-x = t, t^2 = 4/27, t < 0), x^2+y^2 >= rho), output = rootof)

rho <= 1/3

 (2)
> 

QuantifierElimination:-QuantifierEliminate(:-forall([x, y, t], :-Implies(:-And(x^3+y^2-x = t, t^2 = 4/27, t < 0), x^2+y^2 >= rho)))

Error, (in convert/RootOf) there is no root of 3*_Z^2-1 in -348986823692397556565591/604462909807314587353088 .. -174493411846198778282755/302231454903657293676544

  
> 

NULL


 

Download QE_bug.mw

Code: 

QuantifierElimination[QuantifierEliminate](forall([x, y, t], Implies(And(x^3 + y^2 - x = t, And(t^2 = 4/27, t < 0)), x^2 + y^2 >= rho)));

So, is there any bug in Maple's QuantifierElimination package?
Please Wait...