caa a22 4500 463202945 CHVBK 20180405153117.0 cr unu---uuuuu 170326e20071201xx s 000 0 eng 10.1007/s00200-007-0053-x doi (NATIONALLICENCE)springer-10.1007/s00200-007-0053-x Weak quantifier elimination for the full linear theory of the integers [Elektronische Daten] A uniform generalization of Presburger arithmetic [Aless Lasaruk, Thomas Sturm] We describe a weak quantifier elimination procedure for the full linear theory of the integers. This theory 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 or conjunctions. 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 examples demonstrate the applicability of our methods. These examples include problems currently discussed in practical computer science. Springer-Verlag, 2007 Quantifier elimination nationallicence Integer constraint solving nationallicence Implementation nationallicence Lasaruk Aless FORWISS, Universität Passau, 94030, Passau, Germany aut Sturm Thomas FIM, Universität Passau, 94030, Passau, Germany aut Applicable Algebra in Engineering, Communication and Computing Springer-Verlag 18/6(2007-12-01), 545-574 0938-1279 18:6<545 2007 18 200 https://doi.org/10.1007/s00200-007-0053-x text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s00200-007-0053-x text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Lasaruk Aless FORWISS, Universität Passau, 94030, Passau, Germany aut NATIONALLICENCE 700 1- Sturm Thomas FIM, Universität Passau, 94030, Passau, Germany aut NATIONALLICENCE 773 0- Applicable Algebra in Engineering, Communication and Computing Springer-Verlag 18/6(2007-12-01), 545-574 0938-1279 18:6<545 2007 18 200 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer