Cutting-plane proofs in polynomial space (Q1813835)

In order to prove that a system of linear inequalities \(a^ T_ ix\leq b_ i\), \(1\leq i\leq m\), has no integral solution, for \(i=1,\ldots,M\) one may recursively derive a linear inequality \(a^ T_{m+i}x\leq b_{m+i}\), by nonnegative linear combination of previously known linear inequalities and integer roundown of the resulting righthandside. Then, if the last inequality is of the form \(0^ Tx\leq-1\), infeasibility is obvious. Such a system of \(m+M\) inequalities is called a cutting plane proof of length \(M\). The existence of cutting plane proofs for systems with rational coefficients is well-known. Here, for such systems, the existence of a cutting plane proof of length \(O(n^{3n})\) is shown, which can be carried out in polynomial workspace.