First-order logic modulo the theory of integer arithmetic is the basis
for reasoning in many areas, including deductive software verification
and software model checking. While satisfiability checking for ground
formulae in this logic is well understood, it is still an open
question how the general case of quantified formulae can be handled in
an efficient and systematic way. As a possible answer, we introduce a
sequent calculus that combines ideas from free-variable constraint
tableaux with the Omega quantifier elimination procedure.  The
calculus is complete for theorems of first-order logic (without
functions, but with arbitrary uninterpreted predicates), can decide
Presburger arithmetic, and is complete for a substantial fragment of
the combination of both.