@incollection{MIP-0604,
author="A. Lasaruk, T. Sturm",
title="Weak Quantifier Elimination for the Full Linear Theory of the Integers - A Uniform Generalization of Presburger Arithmetic",
institution="Fakult{\"a}t f{\"u}r Mathematik und Informatik, Universit{\"a}t Passau",
year=2006,
number={MIP-0604}
}
We describe a weak quantifier elimination procedure for the full linear theory of the integers. That is a generalization of Presburger arithmetic, where the coefficients are arbitrary polynomials in non-quantified variables. The notion of weak quantifier elimination refers to the fact that the result possibly contains bounded quantifiers. For fixed choices of parameters these bounded quantifiers can be expanded into disjunctions. We furthermore give a corresponding extended quantifier elimination procedure, which delivers besides quantifier-free equivalents also sample values for quantified variables. Our methods are efficiently implemented within the computer logic system REDLOG, which is part of REDUCE. Various application examples demonstrate the applicability of our methods. These examples include problems currently discussed in practical computer science.
