UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

A complete axiomatisation of a fragment of language algebra

Brunet, P; (2020) A complete axiomatisation of a fragment of language algebra. In: Fernandez, M and Muscholl, A, (eds.) LIPIcs : Leibniz International Proceedings in Informatics. (pp. 11:1-11:15). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik: Barcelona, Spain. Green open access

[thumbnail of LIPIcs-CSL-2020-11.pdf]
Preview
Text
LIPIcs-CSL-2020-11.pdf - Published version

Download (450kB) | Preview

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

Type: Proceedings paper
Title: A complete axiomatisation of a fragment of language algebra
Event: 28th EACSL Annual Conference on Computer Science Logic (CSL 2020).
ISBN-13: 9783959771320
Open access status: An open access version is available from UCL Discovery
DOI: 10.4230/LIPIcs.CSL.2020.11
Publisher version: http://dx.doi.org/10.4230/LIPIcs.CSL.2020.11
Language: English
Additional information: licensed under Creative Commons License CC-BY https://creativecommons.org/licenses/by/3.0/
Keywords: Kleene algebra, language algebra, completeness theorem, axiomatisation
UCL classification: UCL
UCL > Provost and Vice Provost Offices
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: https://discovery.ucl.ac.uk/id/eprint/10091600
Downloads since deposit
14Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item