Formalizing the Logic-Automaton Connection.
Stefan Berghofer, Markus Reiter · 2009
Abstract. This paper presents a formalization of a library for automata on bit strings in the theorem prover Isabelle/HOL. 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 the well-known connection between logic and automata theory. 1