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{http://isa-afp.org/entries/Presburger-Automata.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License