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.68250Berghofer, Stefan; Reiter, Markus 2009 all top 5 Cited by 13 Authors 2 Doczkal, Christian 2 Smolka, Gert 2 Urban, Christian 2 Wu, Chunhan 2 Zhang, Xingyuan 1 Berghofer, Stefan 1 Gammie, Peter 1 Krauss, Alexander 1 Lammich, Peter 1 Lochbihler, Andreas 1 Nipkow, Tobias 1 Reiter, Markus 1 Traytel, Dmitry Cited in 2 Serials 4 Journal of Automated Reasoning 1 Journal of Functional Programming Cited in 2 Fields 9 Computer science (68-XX) 3 Mathematical logic and foundations (03-XX) Citations by Year