Presburger Automata

MaRDI QIDQ40317swMATHFDO

Authors Stefan Berghofer, Markus Reiter

Publication date 3 December 2009

Official website https://www.isa-afp.org/entries/Presburger-Automata.html

Cites work

• Diophantine equations, Presburger arithmetic and finite automata
• Formalizing the Logic-Automaton Connection
• Unnamed Publication

Described by source

• Formalizing the Logic-Automaton Connection

Cited in

(22)

• Regular language representations in the constructive type theory of Coq
• MCK
• A formalisation of the Myhill-Nerode theorem based on regular expressions
• Automatic refinement to efficient data structures: a comparison of two approaches
• Two-Way Automata in Coq
• Verified synthesis of knowledge-based programs in finite synchronous environments
• A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
• Myhill-Nerode
• Depth First Search
• CAVA Automata Library
• KBPs
• Gauss Jordan Elimination
• Regular Sets
• Tree Automata
• LTL_to_GBA
• Real_Impl
• Hereditarily Finite Sets
• Finite Automata HF
• Regex_Equivalence
• MSO_Regex_Equivalence
• Verified decision procedures for MSO on words based on derivatives of regular expressions
• Partial and nested recursive function definitions in higher-order logic

This page was built for software: Presburger Automata