Paper Description: MIP-0704

BibTeX entry:

@ incollection{MIP-0704,
author="A. Lasaruk, T. Sturm",
title="Weak Integer Quantifier Elimination Beyond the Linear Case",
institution="Fakult{\"a}t f{\"u}r Informatik und Mathematik, Universit{\"a}t Passau",
year=2007,
number={MIP-0704}
}

Abstract:

We consider the integers using the language of ordered rings extended by ternary symbols for congruence and incongruence. On the logical side we extend first-order logic by bounded quantifiers. Within this framework we describe a weak quantifier elimination procedure for univariately nonlinear formulas. Weak quantifier elimination means that the results possibly contain bounded quantifiers. For fixed choices of parameters these bounded quantifiers can be expanded into finite disjunctions or conjunctions. In univariately nonlinear formulas all congruences and incongruences are linear and their moduls must not contain any quantified variable. All other atomic formulas are linear or contain only one quantified variable, which then may occur with arbitrary degrees. Our methods are efficiently implemented and publicly available within the computer logic system REDLOG, which is part of REDUCE. Various application examples demonstrate the applicability of our new method and its implementation.

Paper itself:

• MIP-0704.pdf