Kleene algebra with commutativity conditions is undecidable
Logic
2024-12-23 v1 Computational Complexity
Computation and Language
Logic in Computer Science
Programming Languages
Abstract
We prove that the equational theory of Kleene algebra with commutativity conditions on primitives (or atomic terms) is undecidable, thereby settling a longstanding open question in the theory of Kleene algebra. While this question has also been recently solved independently by Kuznetsov, our results hold even for weaker theories that do not support the induction axioms of Kleene algebra.
Cite
@article{arxiv.2411.15979,
title = {Kleene algebra with commutativity conditions is undecidable},
author = {Arthur Azevedo de Amorim and Cheng Zhang and Marco Gaboardi},
journal= {arXiv preprint arXiv:2411.15979},
year = {2024}
}
Comments
Published at CSL 2025