Presburger Automata

swMATH ID: 28603
Software Authors: Berghofer, Stefan; Reiter, Markus
Description: Formalizing the logic-automaton connection. 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.
Homepage: https://www.isa-afp.org/entries/Presburger-Automata.html
Dependencies: Isabelle/HOL
Related Software: Archive Formal Proofs; Isabelle/HOL; Myhill-Nerode; Isabelle; HOL; MSO_Regex_Equivalence; Regular Sets; Coq; Finite Automata HF; Hereditarily Finite Sets; Coq/SSReflect; Regex_Equivalence; MONA; Depth First Search; Real_Impl; LTL_to_GBA; Light-weight Containers; Gabow SCC; Tree Automata; CAVA LTL Modelchecker
Cited in: 9 Publications

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
Formalizing the logic-automaton connection. Zbl 1252.68250
Berghofer, Stefan; Reiter, Markus

Citations by Year