Welcome to MathOverflow

Question

2

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?

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?

flag	asked Jul 31 at 14:24 unknown (google) 23●2

1

There is the Coq software. See coq.inria.fr/a-short-introduction-to-coq – Damian Rössler Jul 31 at 14:29

Use the Reduce function in mathematica...maybe that'll help. – S. Sra Jul 31 at 17:42

If you're talking about linear inequalities (as in your examples), this can be written as a feasibility problem of linear programming. The nonlinear case is much more difficult. Still, numerical optimization software may be helpful. – Robert Israel Jul 31 at 18:41

Igor Rivin · Accepted Answer · 2012-07-31 23:34:18Z UTC

6

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).

edited Jul 31 at 23:34

answered Jul 31 at 20:09

Igor Rivin
31.1k●3●37●71

2

In particular, Maple 16 has new features for solving polynomial systems, including polynomial equations, inequations and inequalities. See, for instance, maplesoft.com/support/help/Maple/… – J W Jul 31 at 20:24

Thank you for your answer. My case is linear, so I will be solving a feasibility problem for linear programming to find if the inequality is implied. But this is definitely useful information for me to keep in mind. – unknown (google) Aug 2 at 17:15

PaPiro · Answer 2 · 2012-07-31 14:31:53Z UTC

According Wolfran,

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.

Is there a software to prove or deduce symbolic inequalities?

Remember to vote up questions/answers you find interesting or helpful (requires 15 reputation points)

2 Answers

You can accept an answer to one of your own questions by clicking the check mark next to it. This awards 15 reputation points to the person who answered and 2 reputation points to you.