Automated analysis of regular algebra

DOI10.1007/978-3-642-31365-3_22MaRDI QIDQ2908498zbMATH OpenOpenAlexFDO

Authors Simon Foster, Georg Struth

Publication date 5 September 2012

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-31365-3_22

Mathematics Subject Classification ID

Algebraic theory of languages and automata (68Q70)

Recommendations

• On the fine-structure of regular algebra
• Automated Reasoning in Higher-Order Regular Algebra
• Proof Pearl: regular expression equivalence and relation algebra
• A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
• Completeness results for omega-regular algebras

Cited in

(8)

• On the fine-structure of regular algebra
• Semi-intelligible Isar proofs from machine-generated proofs
• scientific article; zbMATH DE number 2034391 (Why is no real title available?)
• Proving language inclusion and equivalence by coinduction
• A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
• Left omega algebras and regular equations
• scientific article; zbMATH DE number 1696758 (Why is no real title available?)
• Automated Reasoning in Higher-Order Regular Algebra

Describes a project that uses

Uses Software

• HOL
• Isabelle/HOL
• Isabelle

This page was built for publication: Automated analysis of regular algebra

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