Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Lecture
Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
This lecture by the instructor covers the process of quantifier elimination for Presburger Arithmetic, focusing on techniques to eliminate quantifiers from formulas. Starting with simplifying expressions using integer properties, the lecture progresses to handling conjunctions of literals, disjunctive normal form transformation, and exposing variables for elimination. The instructor explains the importance of ensuring coefficients next to variables are one or minus one, and provides examples to illustrate the process. The lecture concludes by discussing the efficiency of quantifier elimination for Presburger Arithmetic and the inherent computational complexity of deciding the truth of quantified formulas.