Formalizing the Logic-Automaton Connection

Title:	Formalizing the Logic-Automaton Connection
Author:	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].
License:	BSD License

Proof outline Proof document

Browse theories

Download this entry

Older releases: Isabelle 2011: afp-Presburger-Automata-2011-02-11.tar.gz Isabelle 2009-2: afp-Presburger-Automata-2010-07-01.tar.gz Isabelle 2009-1: afp-Presburger-Automata-2009-12-12.tar.gz