×

Weak integer quantifier elimination beyond the linear case. (English) Zbl 1141.68704

Ganzha, Victor G. (ed.) et al., Computer algebra in scientific computing. 10th international workshop, CASC 2007, Bonn, Germany, September 16–20, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-75186-1/pbk). Lecture Notes in Computer Science 4770, 275-294 (2007).
Summary: 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 modulus must not contain any quantified variable. All other atomic formulas are linear or contain only one quantified variable, which then may occur there with an arbitrary degree. 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.
For the entire collection see [Zbl 1138.68004].

MSC:

68W30 Symbolic computation and algebraic computation
03C10 Quantifier elimination, model completeness, and related topics

Software:

REDLOG
PDFBibTeX XMLCite
Full Text: DOI