# 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 Conjunctions in DNF

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

Additional information:

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