By the same authors

From the same journal

On the Fine-Structure of Regular Algebra

Research output: Contribution to journalArticle

Full text download(s)

Published copy (DOI)



Publication details

JournalJournal of Automated Reasoning
DatePublished - 3 Dec 2014
Issue number2
Number of pages33
Pages (from-to)165-197
Original languageEnglish


Regular algebra is the algebra of regular expressions as induced by regular language identity. We use Isabelle/HOL for a detailed systematic study of the regular algebra axioms given by Boffa, Conway, Kozen and Salomaa. We investigate the relationships between these systems, formalise a soundness proof for the smallest class (Salomaa’s) and obtain completeness for the largest one (Boffa’s) relative to a deep result by Krob. As a case study in formalised mathematics, our investigations also shed some light on the power of theorem proving technology for reasoning with algebras and their models, including proof automation and counterexample generation.

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations