Minimal set of inequalities I have a set of $m$ linear inequalities in $R^n$, of the form $$ A x \leq b $$ These are automatically generated from the specification of my problem. Many of them could be removed because they are implied by the others. 
I would like to find the minimal set of inequalities, $$ A' x \leq b' $$ such that a solution to the first problem is also a solution to the second, and vice versa. 
One way to do this is to apply Fourier-Motzkin Elimination: I pick one inequality, $a_1 x \leq b_1$, I negate it as $-a_1 x < -b'$, I add it back to the system, and apply FME: if the result is an empty space, then the original inequality can be safely eliminated. Unfortunately, FME is a complex algorithm, and in the worst case it must be applied $m$ times. 
Another possibility is to use linear programming: again, I remove one inequality $a_1 x \leq b$, and I call the remaining set of inequalities $A'' x \leq b''$. Then, I find an optimum for the problem 
$$ \max \;\; a_1 x \\ A'' x \leq b'' $$ using e.g. simplex, and finally I compare the result with $b$: if $a_1 x' < b$ then the inequality can be safely removed, otherwise it must be kept. Again, this has the same complexity of the simplex applied $m$ times (and $m$ is potentially very large). 
Anyone knows a better algorithm?
 A: Using Farkas' lemma, an halfspace $\{x \mid a' x \leq b' \}$  contains the polyhedron $P= \{x |A x \leq b \}$ if and only if there exists $\lambda \in \mathbb{R}^m$ with  $\lambda \geq 0$ (understood component-wise) such that:
\begin{align*}
a' &= \lambda^T A \\
b' &\geq \lambda^T b
\end{align*}
The set 
\begin{align*}
N= \{ (a',b') |  \exists \lambda \geq 0, a' = \lambda^T A, b' \geq \lambda^T b \}
\end{align*}
is called the polar of the polyhedron $P$.
The facets of $P$ are given by the extreme rays of $N$. 
An inequality $a_i x \leq b_i$ will be non-redundant (i.e is not implied by the other) if and only if it is an extreme ray of $N$.
So all you need to do is to compute the conic hull of the $m$ points $(a_1,b_1),...,(a_m,b_m)$ which is more or less equivalent (some gap to fill here) to computing a convex hull. Convex hulls can be computed in $O(m^2)$ using quickhull 
http://www.cse.unsw.edu.au/~lambert/java/3d/quickhull.html
or any other convex hull algorithm. 
A: Here is a proof of the first paragraph of Pascal's answer. It uses directly the separating hyperplane theorem, which states the following.
Given a matrix $A$ and column matrix $b$,
\begin{align}
Ax=b, &\text{ for some column matrix }x\ge0 \\
&\iff \\
y^TA\ge0 &\text{ for some column matrix }y \implies y^Tb\ge0
\end{align}

We put the required proposition into the above form. The premise of the proposition is
\begin{align}
&\begin{bmatrix}
A & b \\
0 & 1
\end{bmatrix}\begin{bmatrix}
-xx_1 \\
x_1
\end{bmatrix}\ge 0  \\
&\iff \\
&\begin{cases} Ax\le b \implies a'^Tx\le b' \\
x_1\ge0 
\end{cases}
\\
&\implies \\
&\begin{bmatrix}a'^T &b'\end{bmatrix} \begin{bmatrix}-xx_1 \\x_1 \end{bmatrix}\ge0
\end{align}
The conclusion of the proposition is
\begin{align}
&\begin{bmatrix}\lambda^T & \lambda_1\end{bmatrix}\begin{bmatrix}
A & b \\
0 & 1
\end{bmatrix}=\begin{bmatrix}a'^T & b'\end{bmatrix}, \text{ for some} \begin{bmatrix}\lambda^T & \lambda_1\end{bmatrix}\ge0 \\
&\iff \\
&\exists \lambda\ge0 \ni
\begin{cases}
\lambda^TA=a'^T \\ 
\lambda^Tb\le b'
\end{cases}
\end{align}
The premise and the conclusion are seen to be equivalent in view of the separating hyperplane theorem as stated above. We have now proved the desired proposition.
