- English only

# Lab for Automated Reasoning and Analysis LARA

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

Running example:

## Normalizing Conjunctions of Literals

We first show that we can bring conjunction of literals into a simpler form.

#### Normal Form of Terms

All terms are built from , so using standard transformations they can be represented as:

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 .

What is the coefficient next to in the resulting formula?

We obtain a formula of the form . Letting , we conclude the formula is equivalent to .

What is the coefficient next to in the resulting formula?

**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 ?

That's it!

## Example

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

Finally :

## Some Improvements

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

## References

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.