Reflecting linear arithmetic: From dense linear orders to presburger arithmetic

This talk presents reflected quantifier elimination procedures for both integer and real linear arithmetic. Reflection means that the algorithms are expressed as recursive functions on recursive data types inside some logic (in our case HOL), are verified in that logic, and can then be applied to the logic itself. After a brief overview of reflection we will discuss a number of quantifier elimination algorithms for the following theories: - Dense linear orders without endpoints. We formalize the standard DNF-based algorithm from the literature. - Linear real arithmetic. We present both a DNF-based algorithm extending the case of dense linear orders and an optimized version of the algorithm by Ferrante and Rackoff [3]. - Presburger arithmetic. Again we show both a naive DNF-based algorithm and the DNF-avoiding one by Cooper [2]. We concentrate on the algorithms and their formulation in Isabelle/HOL, using the concept of locales to allow modular definitions and verification. Some of the details can be found in joint work with Amine Chaib [1].