License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2020.11
URN: urn:nbn:de:0030-drops-116546
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/11654/
Go to the corresponding LIPIcs Volume Portal

Brunet, Paul

A Complete Axiomatisation of a Fragment of Language Algebra

pdf-format:
LIPIcs-CSL-2020-11.pdf (0.4 MB)

Abstract

We consider algebras of languages over the signature of reversible Kleene lattices, that is the regular operations (empty and unit languages, union, concatenation and Kleene star) together with intersection and mirror image. We provide a complete set of axioms for the equational theory of these algebras. This proof was developed in the proof assistant Coq.

BibTeX - Entry

@InProceedings{brunet:LIPIcs:2020:11654,
  author =	{Paul Brunet},
  title =	{{A Complete Axiomatisation of a Fragment of Language Algebra}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{11:1--11:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Maribel Fern{\'a}ndez and Anca Muscholl},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/11654},
  URN =		{urn:nbn:de:0030-drops-116546},
  doi =		{10.4230/LIPIcs.CSL.2020.11},
  annote =	{Keywords: Kleene algebra, language algebra, completeness theorem, axiomatisation}
}

Keywords: Kleene algebra, language algebra, completeness theorem, axiomatisation
Collection: 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)
Issue Date: 2020
Date of publication: 06.01.2020
Supplementary Material: Coq formalisation: https://github.com/monstrencage/LangAlg

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI