# Formalizing the Logic-Automaton Connection

 Title: Formalizing the Logic-Automaton Connection Authors: Stefan Berghofer and Markus Reiter Submission date: 2009-12-03 Abstract: 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]. BibTeX: @article{Presburger-Automata-AFP, author = {Stefan Berghofer and Markus Reiter}, title = {Formalizing the Logic-Automaton Connection}, journal = {Archive of Formal Proofs}, month = dec, year = 2009, note = {\url{https://isa-afp.org/entries/Presburger-Automata.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License