Performance Issues: Solving Inequality with Multiple Assumptions in Mathematica

Question

I need to prove the inequality (or find a counter example), given several assumptions (also inequalities). Unfortunately, the proven inequality is a rather long and complex expression. There are about 15 variables, and FullSimplify output fills several A4 pages. For examples with smaller variables, FindInstance helps find a counterexample or gives the result {}, if true. I also tried using Reduce as follows:

 Reduce[ Implies[ assumtion1 && assumtion2, inequality ], Reals ] 

For simple examples, this prints "True" if the inequality holds. But in my case, after several hours of work, Mathematica needed 5-6 GB of RAM (and sharing), so I had to cancel this process.

Is there anything I could do with Mathematica to improve performance?

Answer 1

You will find a very good article on MMA CAD algorithms here.

The cylindrical algebraic expansion (CAD) that Mma uses is scaled with double exponential behavior in the number of variables.

Newer methods are double exponential in the number of quantum interlaces.

I think you will not be able to use only the internal Mma engine, but you can overturn your own, based on the symmetry of your problem (if any)