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.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.