Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

A complete axiomatisation of reversible Kleene lattices

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.
Complete list of metadata

Cited literature [9 references]  Display  Hide  Download
Contributor : Paul Brunet Connect in order to contact the contributor
Submitted on : Monday, April 22, 2019 - 11:58:30 AM
Last modification on : Monday, May 13, 2019 - 10:48:50 AM


  • HAL Id : hal-02024864, version 2
  • ARXIV : 1902.08048


Paul Brunet. A complete axiomatisation of reversible Kleene lattices. 2019. ⟨hal-02024864v2⟩



Les métriques sont temporairement indisponibles