# A complete axiomatisation of reversible Kleene lattices

## TL;DR

This paper provides a complete axiomatization of reversible Kleene lattices, algebraic structures that include regular operations, intersection, and mirror image, with a formal proof developed in Coq.

## Contribution

It introduces the first complete set of axioms for the equational theory of reversible Kleene lattices, expanding algebraic understanding of language operations.

## Key findings

- Complete axiomatization achieved for reversible Kleene lattices
- Formal proof developed in Coq proof assistant
- Enhances algebraic tools for language theory

## 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.