Lab 03: Quantifier Elimination
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.
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:
Eliminate quantifiers in the following formula in Presburger arithmetic.