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)