Lecturecise 03: Presburger Arithmetic and Quantifier Elimination

Further Notes and Examples of QE

Applications of Quantifier Elimination

Quantifier Elimination Definition

QE from Conjunction of Literals Suffices

Simple QE for Dense Linear Orders

Simple QE for Integer Difference Inequalities

Definition of Presburger Arithmetic

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

Exercise: eliminate quantifiers in the following formula in Presburger arithmetic.

\exists y. \exists x. x < -2 \wedge 1 - 5y < x \wedge 1 + y < 13x

More Efficient Handling of Conjunctions in DNF

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

Additional information: