Séminaire, 5 avril 2018
Exposés
 11:00: Amina Doumane (LIP, ÉNS Lyon), Completeness for identityfree Kleene Lattices

We provide a finite set of axioms for identityfree Kleene lattices, which we prove sound and complete for the equational theory of their relational models. This equational theory was previously proved to coincide with that of language models and to be ExpSpace complete; expressions of the corresponding syntax moreover make it possible to denote precisely those languages of graphs that can be accepted by Petri automata. Finite axiomatisability was missing to obtain the same picture as for Kleene algebra, regular expressions, and (word) automata.
Our proof builds on the completeness theorem for Kleene algebra, and on a novel automata construction that makes it possible to extract axiomatic proofs using a Kleenelike algorithm.