# 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”?

Maple

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
=

```

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  (over ℝ²) should at least be x2y2＞1, yet convert(Or,function,map2(`?()`,And,RealDomain[solve](And(y*y+x*x>0^0),[x,y]))); simply returns , 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?

﻿