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.
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 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 |
Archive Staff Only
 |
View Item |
