Algorithmic Quantifier Elimination
Overview
| Lecturer | Thomas Sturm |
|---|---|
| Start | Tuesday, April 11, 2023, 8: 30 a.m. |
| Time (Lecture) | Tuesdays, 8: 30– 10 s.t. |
| Time (Excercises) | Wednesdays 8: 30– 10 s.t. |
| Place | Room 630, building E1 5(6 th floor) for both lecture and excercises |
Prerequisites
Basic knowledge in computer science, in particular in first-order logic
Quantifier Elimination in a Nutshell
Consider the formula ∀x ∃y (x² + xy + b > 0 ∧ x + ay² + b ≤ 0). A quantifier elimination algorithm for the real numbers can compute an equivalent formula without any quantifiers, which in this example would be a < 0 ∧ b > 0. Such a quantifier-free formula has several advantages over the original formula. Dynamically, for given choices of a and b, it can be straightforwardly evaluated to either "true" or "false". Structurally, the set of all "true" choices of (a, b) define a binary relation on the real numbers. The quantifier-free formula provides a better intuition of that relation than the original one.
Quantifier elimination is possible in many interesting domains (e.g. in the real numbers, complex numbers) but not generally (e.g. not in the rational numbers), sometimes only for certain classes of formulas (e.g. linear formulas over the integers, known as Presburger Arithmetic).
Quantifier elimination is used "under the hood" in Automated Reasoning when algebraically theories are involved. Examples are superposition modulo theories and Satisfiability Modulo Theories (SMT) solving. Direct applications of quantifier elimination include circuit analysis/design/diagnosis, verification, hybrid control theory, geometric proving, computational geometry, motion planning, chemical reaction network theory, systems biology.
From a formal point of view, quantifier elimination provides a framework for a formally clean management of parametric settings.
Open source software for quantifier elimination is being developed at RG1.
Lecture Notes
Lecture notes are available here: 2023-07-14-lnqe.pdf
If you discover any typos or other problems in the notes, please send an email with subject "LNQE" to sturm@mpi-inf.mpg.de. Thanks!
Come back to check for updates!
Practical Part
The exercises comprise prototypical implementations of the algorithms discussed throughout the course. The programming language is Python 3. A suitable framework will be provided.
Details: https://people.mpi-inf.mpg.de/~sturm/teaching/143421/logic1/