On the Fine-Structure of Regular Algebra

Simon David Foster; Georg Struth

doi:10.1007/s10817-014-9318-9

On the Fine-Structure of Regular Algebra

Simon David Foster, Georg Struth

Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

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 language	English
Pages (from-to)	165-197
Number of pages	33
Journal	Journal of Automated Reasoning
Volume	54
Issue number	2
DOIs	https://doi.org/10.1007/s10817-014-9318-9
Publication status	Published - 3 Dec 2014

Access to Document

10.1007/s10817-014-9318-9

regalg
© Springer Science+Business Media Dordrecht 2014. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details
Accepted author manuscript, 209 KB

Simon David Foster
- simon.fosteryork.acuk
- Computer Science - Lecturer
Person: Academic

Cite this

@article{13724ac503564c52bb2e36d4099aaae1,

title = "On the Fine-Structure of Regular Algebra",

abstract = "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{\textquoteright}s) and obtain completeness for the largest one (Boffa{\textquoteright}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.",

author = "Foster, {Simon David} and Georg Struth",

year = "2014",

month = dec,

day = "3",

doi = "10.1007/s10817-014-9318-9",

language = "English",

volume = "54",

pages = "165--197",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer",

number = "2",

}

TY - JOUR

T1 - On the Fine-Structure of Regular Algebra

AU - Foster, Simon David

AU - Struth, Georg

PY - 2014/12/3

Y1 - 2014/12/3

N2 - 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.

AB - 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.

U2 - 10.1007/s10817-014-9318-9

DO - 10.1007/s10817-014-9318-9

M3 - Article

SN - 0168-7433

VL - 54

SP - 165

EP - 197

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 2

ER -

On the Fine-Structure of Regular Algebra

Abstract

Access to Document

Profiles

Simon David Foster

Cite this