# Techniques for proving that a set of constraints over the integers are inconsistent

I have a problem which boils down to showing that a set of constraints has no solutions. A simplified version of this constraint system would be the following system:

$$\left\{ \begin{array}{l} \sum_{i=1}^n a_i\leq k\\ 0\leq a_i,\;\;i=1,\ldots,n\\ f = \sum_{i=1}^n a_ig_i\\ 0\leq r_i,\;\; i=1,\ldots,n\\ r_i\leq a_il_i,\;\;i=1,\ldots,n \end{array} \right.$$

where the $k,a_i,r_i,l_i$ are integer valued variables. Furthermore, $f$ is a linear expression in the variables $k,r_1,\ldots,r_n,l_1,\ldots,l_n$ and each $g_i$ is a linear expression in the variables $l_1,\ldots,l_n$.

The problem is that the third equation and the last set of equations are non-linear. I'm aware that a general quadratic constraint problem allows us to encode any Diophantine problem, which is undecidable. I've been looking at the literature for any special cases that could apply here, but almost everywhere an assumption is made that the problem is already bounded and then an attempt is made to find a solution as quickly as possible. This makes as a simplifying assumption already a step we need to prove.

I'm interesting in showing that emptyness of the solution set of the system is decidable. Probabilistic methods do not cut it, since this pops up in a theorem proving context.

Any pointers to relevant literature or ideas on linearizing or converting it to something that can be solved would be appreciated.