2026-08-07T14:08:16Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:22793 2025-02-03T10:18:31Z ddc:004 open_access

Kleene Algebra with Commutativity Conditions Is Undecidable Azevedo de Amorim, Arthur Zhang, Cheng Gaboardi, Marco Kleene Algebra Hypotheses Complexity 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Arthur Azevedo de Amorim and Cheng Zhang and Marco Gaboardi 2025 Is Part Of LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2025.36 urn:nbn:de:0030-drops-227933 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.36 eng https://creativecommons.org/licenses/by/4.0/legalcode