Formalizing the Logic-Automaton Connection

DOI10.1007/978-3-642-03359-9_12zbMath1252.68250OpenAlexW2159882284MaRDI QIDQ3183526

Stefan Berghofer, Markus Reiter

Publication date: 20 October 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-03359-9_12

Mathematics Subject Classification ID

Related Items (9)

Regular language representations in the constructive type theory of Coq ⋮ Automatic refinement to efficient data structures: a comparison of two approaches ⋮ Verified decision procedures for MSO on words based on derivatives of regular expressions ⋮ Partial and nested recursive function definitions in higher-order logic ⋮ Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments ⋮ A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl) ⋮ Presburger Automata ⋮ Two-Way Automata in Coq ⋮ A formalisation of the Myhill-Nerode theorem based on regular expressions

Uses Software

• Isabelle
• Isabelle/HOL
• MONA
• Depth First Search
• Archive Formal Proofs

Cites Work

• Proof synthesis and reflection for linear arithmetic
• Verified Decision Procedures on Context-Free Grammars
• Linear Quantifier Elimination
• Partial Recursive Functions in Higher-Order Logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Formalizing the Logic-Automaton Connection