Formalizing the Logic-Automaton Connection

Stefan Berghofer 🌐 and Markus Reiter

December 3, 2009

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


This work presents a formalization of a library for automata on bit strings. It forms the basis of a reflection-based decision procedure for Presburger arithmetic, which is efficiently executable thanks to Isabelle's code generator. With this work, we therefore provide a mechanized proof of a well-known connection between logic and automata theory. The formalization is also described in a publication [TPHOLs 2009].
BSD License


Theories of Presburger-Automata