Formalizing the Logic-Automaton Connection

DOI10.1007/978-3-642-03359-9_12MaRDI QIDQ3183526zbMATH OpenOpenAlexFDO

Authors 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

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Automata and formal grammars in connection with logical questions (03D05)

Recommendations

• scientific article; zbMATH DE number 1342250
• Büchi automata optimisations formalised in Isabelle/HOL
• scientific article; zbMATH DE number 5872401
• scientific article; zbMATH DE number 1670757
• scientific article; zbMATH DE number 2038699

Cites work

• Combining WS1S and HOL
• scientific article; zbMATH DE number 1696436 (Why is no real title available?)
• scientific article; zbMATH DE number 1223628 (Why is no real title available?)
• scientific article; zbMATH DE number 1538036 (Why is no real title available?)
• scientific article; zbMATH DE number 2085164 (Why is no real title available?)
• Linear Quantifier Elimination
• Partial Recursive Functions in Higher-Order Logic
• Proof synthesis and reflection for linear arithmetic
• Verified Decision Procedures on Context-Free Grammars

Cited in

(13)

• Regular language representations in the constructive type theory of Coq
• Formal logics of discovery and hypothesis formation by machine
• 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)
• Presburger Automata
• scientific article; zbMATH DE number 1341537 (Why is no real title available?)
• scientific article; zbMATH DE number 1342250 (Why is no real title available?)
• scientific article; zbMATH DE number 2038699 (Why is no real title available?)
• Verified decision procedures for MSO on words based on derivatives of regular expressions
• Partial and nested recursive function definitions in higher-order logic

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3183526)