Bounding Variables in Presburger Arithmetic

We can use insights from quantifier elimination to obtain alternative algorithms for deciding formulas.

Define and for all .

Bounds Showing Membership in 2EXPSPACE

Let denote the maximum of the constant and of all constants ocurruring in the formula .

Theorem (Oppen): There exists a constant such that the following is true. If is a formula of Presburger arithmetic with quantifiers, then when Cooper's procedure is applied to , every integer constant encountered is bounded by Lemma (Ferrante, Rackhoff): There exists a constant such that the following is true. Let be the formula , where is quantifier-free and is or for each , , and let . Then is true iff where means .

Bounded Quantifier Alternation

Example: if has no quantifiers, then these two formulas have one quantifier alternation:  and this formula has two quantifier alternations: Definition: A formula in prenex form has quantifier alternations iff it is the form where for the same , all quantifiers  are the same type (either all are or all are ), and for and the quantifiers are of different type.

Theorem (Reddy, Loveland, 1978): If is a closed Presburger arithmetic formula of size with quantifier alternations, where are quantifiers and is quantifier-free, then is true iff the formula with bounded quantifiers is true for some .

In general, it is often quantifier alternations that cause high complexity of the decision procedure, not quantifiers themselves.

• Reddy, Loveland: Presburger Arithmetic with Bounded Quantifier Alternation, pdf
• Lararuk, Sturm: Weak quantifier elimination for the full linear theory of the integers, pdf
• Ferrante, Rackoff: A Decision Procedure for the First-Order Theory of Addition with Order, pdf (NOTE: this is for real numbers, not integers)