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. © 2009 Springer.
Cite
CITATION STYLE
Berghofer, S., & Reiter, M. (2009). Formalizing the logic-automaton connection. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5674 LNCS, pp. 147–163). https://doi.org/10.1007/978-3-642-03359-9_12
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
