Kleene algebra with commutativity conditions is undecidable
This resolves a fundamental problem in theoretical computer science and algebra, with implications for verification and logic, though it is incremental as it builds on prior work.
The paper proves that the equational theory of Kleene algebra with commutativity conditions on primitives is undecidable, settling a longstanding open question, and shows this holds even for weaker theories without induction axioms.
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.