Reflecting linear arithmetic: From dense linear orders to presburger arithmetic

Research output: Contribution to journalConference articlepeer-review


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].

Original languageEnglish
Pages (from-to)1
Number of pages1
JournalCEUR Workshop Proceedings
StatePublished - 2007
Event4th International Verification Workshop, VERIFY 2007, Affiliated with the 21st Conference on Automated Deduction, CADE 2007 - Bremen, Germany
Duration: 15 Jul 200716 Jul 2007


Dive into the research topics of 'Reflecting linear arithmetic: From dense linear orders to presburger arithmetic'. Together they form a unique fingerprint.

Cite this