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.
More Efficient Handling of Conjunctions in DNF
More efficient handling of disjunctions and divisibility: see the Calculus of Computation textbook
Additional information: