Department of Information Technology

Formalizing the Logic-Automaton Connection


Stefan Berghofer

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.

Back to the seminar page

Updated  2009-04-16 06:54:43 by Frédéric Haziza.