Some applications of automated deduction require reasoning modulo some form of integer 
arithmetic. Unfortunately, theory reasoning support for the integers in current theorem provers is
sometimes too weak for practical purposes. In particular, the family of Satisfiability Modulo Theories 
solvers [NOT06] lack support for quantifiers and resort to incomplete or inefficient heuristics to 
deal with quantified formulas. Also, theory reasoning techniques developed within first-order theorem proving are often impractical as they require enumeration of complete sets of theory unifiers 
(in particular those in the tradition of Stickel's Theory Resolution [Sti85]) or feature only weak or 
no redundancy criteria (for instance, Bürckert’s Constraint Resolution [Buer90]). 

In this paper we propose a novel calculus for first-order logic modulo Linear Integer Arithmetic 
(LIA) that avoids these problems. The calculus requires a decision procedure for the 
$\forall\exists$ 
fragment of LIA instead of complete LIA-unification procedure, and is amenable to strong redundancy 
criteria. It is derived from the Model Evolution calculus [BT03], a first-order logic version of 
the propositional DPLL procedure. The main data structure of that calculus is the context, which 
provides a compact representation of certain Herbrand interpretations. The new calculus builds in 
its core on a version of contexts modulo LIA. More precisely, the contexts (and the calculus) deal 
with conservative extensions of the integers structure by free predicate and constant symbols. 

In the talk we present the basic ideas of the calculus and its theoretical properties, restricted 
for now to the case of free predicate and constant symbols ranging over finite integer domains.