The classical algebraic modelling approach for integer programming (IP) is
not suitable for some real world IP problems, since the algebraic formulati
ons allow only for the description of mathematical relations. not logical r
elations. In this paper, we present a language L+ for IF, in which we write
logical specification of an IP problem. L+ is a language based on the pred
icate logic, but is extended with meta predicates such as at least(m, S), w
here m is a non-negative integer, meaning that at least m predicates in the
set S of formulas hold. The meta predicates facilitate reasoning about a m
odel of an IP problem rigorously and logically. L+ is executable in the sen
se that formulas in L+ are mechanically translated into a set of mathematic
al formulas, called IP formulas, which most of existing IP solvers accept.
We give a systematic method for translating formulas in Ci to IP formulas.
The translation is rigorously defined, verified and implemented in Mathemat
ica 3.0. Our work follows the approach of McKinnon and Williams, and elabor
ated the language in that (1) it is rigorously defined, (2) transformation
to IP formulas is more optimised and verified, and (3) the transformation i
s completely given in Mathematica 3.0 and is integrated into IP solving env
ironment as a tool for IF.