Proof Pearl: regular expression equivalence and relation algebra

DOI10.1007/s10817-011-9223-4zbMath1269.68090OpenAlexW1968602591MaRDI QIDQ2392416

Alexander Krauss, Tobias Nipkow

Publication date: 1 August 2013

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-011-9223-4

zbMATH Keywords

regular expressionsdecision procedure\texttt{Isabelle/HOL}

Mathematics Subject Classification ID

Related Items (18)

A Formalisation of Finite Automata Using Hereditarily Finite Sets ⋮ Automated Reasoning in Higher-Order Regular Algebra ⋮ Deciding Regular Expressions (In-)Equivalence in Coq ⋮ On Completeness of Omega-Regular Algebras ⋮ Regular language representations in the constructive type theory of Coq ⋮ Deciding Synchronous Kleene Algebra with Derivatives ⋮ Programming and automating mathematics in the Tarski-Kleene hierarchy ⋮ POSIX lexing with derivatives of regular expressions ⋮ Proving language inclusion and equivalence by coinduction ⋮ Verified verifying: SMT-LIB for strings in Isabelle ⋮ Verified decision procedures for MSO on words based on derivatives of regular expressions ⋮ Completeness for Identity-free Kleene Lattices ⋮ Unnamed Item ⋮ Building program construction and verification tools from algebraic principles ⋮ POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl) ⋮ A Decision Procedure for Regular Expression Equivalence in Type Theory ⋮ Deciding Kleene algebra terms equivalence in Coq ⋮ A formalisation of the Myhill-Nerode theorem based on regular expressions

Uses Software

• Isabelle
• Isabelle/HOL
• CeTA
• Archive Formal Proofs
• Regular Sets

Cites Work

• Unnamed Item
• Unnamed Item
• A completeness theorem for Kleene algebras and the algebra of regular events
• A Decision Procedure for Bisimilarity of Generalized Regular Expressions
• Certification of Termination Proofs Using CeTA
• Code Generation via Higher-Order Rewrite Systems
• Regular-expression derivatives re-examined
• Derivatives of Regular Expressions
• An Efficient Coq Tactic for Deciding Kleene Algebras

This page was built for publication: Proof Pearl: regular expression equivalence and relation algebra