Unified Decision Procedures for Regular Expression Equivalence

DOI10.1007/978-3-319-08970-6_29zbMath1416.68175OpenAlexW260922524MaRDI QIDQ2879269

Dmitriy Traytel, Tobias Nipkow

Publication date: 8 September 2014

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-08970-6_29

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Related Items (14)

Quotients of Bounded Natural Functors ⋮ A Formalisation of Finite Automata Using Hereditarily Finite Sets ⋮ Manipulation of regular expressions using derivatives: an overview ⋮ Deciding Synchronous Kleene Algebra with Derivatives ⋮ Derivatives and partial derivatives for regular shuffle expressions ⋮ Unnamed Item ⋮ Location automata for regular expressions with shuffle and intersection ⋮ Verified decision procedures for MSO on words based on derivatives of regular expressions ⋮ Unnamed Item ⋮ Location based automata for expressions with shuffle ⋮ A mesh of automata ⋮ Regex_Equivalence ⋮ Two-Way Automata in Coq ⋮ On the fine-structure of regular algebra

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• MSO_Regex_Equivalence

This page was built for publication: Unified Decision Procedures for Regular Expression Equivalence