Effective Quantifier Elimination for Presburger Arithmetic with Infinity

We consider Presburger arithmetic extended by infinity. For this we give an effective quantifier elimination and decision procedure which implies also the completeness of our extension. The asymptotic worst-case complexity of our procedure is bounded by a function that is triply exponential in the input word length, which is known to be a tight bound for regular Presburger arithmetic. Possible application areas include quantifier elimination and decision procedures for Boolean algebras with cardinality constraints, which have recently moved into the focus of computer science research for software verification, and deductive database queries.

• Type: Conference
• Year: 2009
• Where: CASC
• Authors: Aless Lasaruk, Thomas Sturm
• Keywords: CASC 2009, Decision Procedures, Effective Quantifier Elimination, Mathematics, Quantifier Elimination