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