# 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.

## References

• 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)