Presburger Automata
From MaRDI portal
swMATH28603MaRDI QIDQ40317FDOQ40317
Author name not available (Why is that?)
Official website: https://www.isa-afp.org/entries/Presburger-Automata.html
Cited In (22)
- A formalisation of the Myhill-Nerode theorem based on regular expressions
- Regular language representations in the constructive type theory of Coq
- A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
- MCK
- CAVA Automata Library
- Depth First Search
- Gauss Jordan Elimination
- KBPs
- Myhill-Nerode
- Regular Sets
- Finite Automata HF
- Hereditarily Finite Sets
- LTL_to_GBA
- Real_Impl
- Tree Automata
- MSO_Regex_Equivalence
- 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
- Two-Way Automata in Coq
- Automatic refinement to efficient data structures: a comparison of two approaches
- Verified synthesis of knowledge-based programs in finite synchronous environments
This page was built for software: Presburger Automata
