Quantifier Elimination for Presburger Arithmetic
(In the language over integers from Definition of Presburger Arithmetic.)
We consider elimination of a quantifier from a conjunction of literals (because QE from Conjunction of Literals Suffices).
Normalizing Conjunctions of Literals
We first show that we can bring conjunction of literals into a simpler form.
Normal Form of Terms
We call such term a linear term.
Normal Form for Literals
Relation symbols: , , .
We obtain a disjunction of conjunctions of literals of the form and where are of the form
Exposing the Variable to Eliminate
By previous transformations, we are eliminating from conjunction of and where is a linear term.
Coefficient next to : To eliminate from such conjunction, we wish to ensure that the coefficient next to is one or minus one.
Observation: is equivalent to and is equivalent to for a positive integer.
If are all coefficients next to in the formula, let be a positive integer such that for all , (for example, let be the least common multiple of ). Multiply each literal where occurs in subterm by constant .
We obtain a formula of the form . Letting , we conclude the formula is equivalent to .
Lower and upper bounds: Consider the coefficient next to in . If it is , move the term to left side. If it is , move the remaining terms to the left side. We obtain formula of the form
If there are no divisibility constraints (), what is the formula equivalent to?
Replacing variable by test terms: There is a an alternative way to express the above condition by replacing with where do not contain . This is a common technique in quantifier elimination. Note that if holds then certainly .
What are example terms when and ? Hint: ensure that at least one of them evaluates to .
What if i.e. we have additional divisibility constraints?
Note that if holds then also holds.
That's it for .
What if ?
Consider verification condition from Symbolic Execution for Example Integer Program.
How can we prove such verification condition?
The invariant of this code example is :
We have to find out if is satisfiable.
We can eliminate quantifiers with equalities: and
becomes , and can be removed
Avoid transforming to conjunctions of literals: work directly on negation-normal form.
- the technique is similar to what we described for conjunctive normal form
This is the Cooper's algorithm
- Reddy, Loveland: Presburger Arithmetic with Bounded Quantifier Alternation (gives a slight improvement of the original Cooper's algorithm)
- Section 7.2 of the Calculus of Computation Textbook
The presentation in thes notes follows Appendix of this report, which also contains further references.
See Section 7.2 of the Calculus of Computation Textbook for a description of more efficient Cooper's algorithm.