2026-07-25T12:37:12Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11654 2024-03-06T10:48:42Z ddc:004 open_access

A Complete Axiomatisation of a Fragment of Language Algebra Brunet, Paul Kleene algebra language algebra completeness theorem axiomatisation 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Paul Brunet 2020 Is Part Of LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2020.11 urn:nbn:de:0030-drops-116546 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.11 eng https://creativecommons.org/licenses/by/3.0/legalcode