# Lab 03: Quantifier Elimination

## Exercise 1

If instead of good states we look at the complement set of error states, the corresponds to doing backwards.
In other words, for , , the following holds:

Prove this statement.

## Quantifier Elimination

QE for Presburger Arithmetic
Here is also a PDF that does not have any folding/missing content issues.

More efficient handling of disjunctions and divisibility: see the Calculus of Computation textbook

## Synthesis through Quantifier Elimination

Recall Hoare triple:

We have also seen how to do the following (at least for Presburger arithmetic):

• given , check if the condition holds
• given and , compute the strongest
• given and , compute the weakest

How can we compute:

• given and compute the largest relation such that the triple holds (hint: it is easy!)

But how to do functional synthesis:

• given , find a (deterministic) function in our programming language such that whenever .

Here is one approach:

### Exercise 2

Eliminate quantifiers in the following formula in Presburger arithmetic.