Is there a software to prove or deduce symbolic inequalities? - MathOverflow most recent 30 from http://mathoverflow.net 2013-06-19T04:09:39Z http://mathoverflow.net/feeds/question/103613 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/103613/is-there-a-software-to-prove-or-deduce-symbolic-inequalities Is there a software to prove or deduce symbolic inequalities? unknown (google) 2012-07-31T14:24:13Z 2012-07-31T23:34:18Z <p>I have a bunch of inequalities, and I'm trying to see if another inequality can be deduced from the first bunch. For example, assuming that $a \leq b$ and $c \leq d$, we can deduce that $a + c \leq b + d$, but we cannot deduce that $a + d \leq b + c$. Is there some software that allows me to take some inequalities which are assumed to be true as input, and to check if another input inequality can be deduced or proved from these earlier inequalities?</p> <p>I am most familiar with MATLAB and it doesn't seem to do this. I realized that I could hack it and say for example $b = a + p$, $d = c + q$ with $p, q \geq 0$, then just writing $b + d - (a + c)$ and asking MATLAB to simplify the expression, and noticing that all the $p, q$ terms are nonnegative. But is there a more natural way to do this?</p> http://mathoverflow.net/questions/103613/is-there-a-software-to-prove-or-deduce-symbolic-inequalities/103614#103614 Answer by PaPiro for Is there a software to prove or deduce symbolic inequalities? PaPiro 2012-07-31T14:31:53Z 2012-07-31T14:31:53Z <p>According <a href="http://reference.wolfram.com/mathematica/guide/Inequalities.html" rel="nofollow">Wolfran</a>,</p> <p><em>Mathematica uses a large number of original algorithms to provide automatic systemwide support for inequalities and inequality constraints. Whereas equations can often be solved in terms of numbers, even representing solution sets for inequalities is only made possible by Mathematica's symbolic capabilities.</em></p> http://mathoverflow.net/questions/103613/is-there-a-software-to-prove-or-deduce-symbolic-inequalities/103630#103630 Answer by Igor Rivin for Is there a software to prove or deduce symbolic inequalities? Igor Rivin 2012-07-31T20:09:41Z 2012-07-31T23:34:18Z <p>As @Robert Israel points out, the linear case is MUCH easier than the general case, and the really general case (arbitrary inequalities of the form $f(\mathbf{x}) \geq 0$) is clearly undecidable, but if the inequalities are polynomial, this is the problem of "quantifier elimination over real closed fields", which you can google. The first algorithm was "Tarski's algorithm", there have been many improvements since, most of them used by computer algebra systems (Mathematica, Maple, etc).</p>