Formalizing the Logic-Automaton Connection
- Date and Time
Thursday, April 23rd, 2009, at 13.30.
Polacksbaken, room 1146
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.