Advanced Search

Question: How to (fully) simplify logical combinations of equations, inequalities, and inequations (or nonequalities) using contextual information WITHOUT “overkill”?

Question:How to (fully) simplify logical combinations of equations, inequalities, and inequations (or nonequalities) using contextual information WITHOUT “overkill”?

sursumCorda 1064 Maple
boolean simplification logic
March 09 2024
0

Here is a "toy" instance. 
As the title suggests, I would like to simplify the following boolean combinations: (Note that the context should be taken into account.) 

formula__0 := 
 convert(And(
   Non(`xor`(Or(0 >- 0, y ** 3=x), 
     And(((y*x - 0^0)^2 + (y*y - x*x)^2)*(y^2 + x^2) > 
       0, 0 <- (y**3 - x)*(y - x**3)**3, 
      `implies`(y + x*2 >= y ** 3*2 + x**3, 
       Or(y + x < y*y*y + x*x*x)), Not((y**3 - x)*(y - x**3) = 0), 
      0 >= 0), y <> x*x*x))), 'boolean_function'):

Regretfully, the built-in command simplify is unable to simplify formula__0: 

simplify(formula__0, assume = real); # only rudimentary simplifications 
 = 
RealDomain:-simplify(convert(And(Non(`xor`(Or(0>-0,y**3=x),And(((y*x-0^0)^2+(y*y-x*x)^2)*(y^2+x^2)>0,0<-(y**3-x)*(y-x**3)**3,`implies`(y+x*2>=y**3*2+x**3,Or(y+x<y*y*y+x*x*x)),Not((y**3-x)*(y-x**3)=0),0>=0),y<>x*x*x))),'boolean_function'))

The library function SMTLIB:-Simplify seems to simplify it, but the result is incorrect: 

(SMTLIB:-Simplify(formula__0) assuming real); # check {y = 1, x = 0} 
 = 
                    /   /   / 3           3\\\
                 And\Not\And\y  = x, y = x ///

The only procedure I can find that is capable of rewriting it appears to be RealDomain:-solve: 

RealDomain:-solve(formula__0, 'allsolutions'); # see below 
 = 
Warning, solutions may have been lost
    /            3\    /     3       \    /     3        \   
   { x = x, y = x  }, { x = y , y = y }, { y = x , x < -1 }, 
    \             /    \             /    \              /   

      /     3              \    /     3        \   
     { y = x , 0 < x, x < 1 }, { x = y , y < -1 }, 
      \                    /    \              /   

      /     3              \ 
     { x = y , 0 < y, y < 1 }
      \                    /

Nevertheless, this is more or less overkill, since a complete solution set is somewhat unnecessary, and in practice, an simplified and compact but presumably unsolved form is more applicable to further manipulations. (For example, the simplest form of And(y*y + x*x > 0^0): (over ℝ²) should at least be x2＋y2＞1, yet convert(Or,function,map2(`?()`,And,RealDomain[solve](And(y*y+x*x>0^0),[x,y]))); simply returns sort(convert(Or,function,map2(`?()`,And,RealDomain[solve](And(y*y+x*x>0^0),[x,y]))),[x,y]), which is definitely unsuitable here.) (A more real example can be found in the Ex３ of this compressed file.)

I believe that this is a common problem; curiously, I cannot find any related questions in this forum. So, are such simplifications (similar to SLFQ) available in Maple? 
Please Wait...