Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Brunet, Paul http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-116546
URL:

A Complete Axiomatisation of a Fragment of Language Algebra

pdf-format:


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
Seminar: 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)
Issue date: 2020
Date of publication: 2020


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