Slides

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:

• List of Theories Admitting QE
• Quantifier Elimination for Real Polynomials
• Extending Languages of Decidable Theories