On the Fine-Structure of Regular Algebra

Simon David Foster, Georg Struth

Research output: Contribution to journalArticlepeer-review


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.
Original languageEnglish
Pages (from-to)165-197
Number of pages33
JournalJournal of Automated Reasoning
Issue number2
Publication statusPublished - 3 Dec 2014

Cite this