证明带交换律的Kleene代数等式理论不可判定

Kleene algebra with commutativity conditions is undecidable

• 通过引入原子项的交换律条件，扩展Kleene代数
• 证明其等式理论在任意情况下均不可判定
• 适用于逻辑与形式验证领域的研究者

我们证明了带有原子项交换律条件的Kleene代数等式理论是不可判定的，从而解决了该领域长期悬而未决的开放问题。尽管此问题最近已被Kuznetsov独立解决，但我们的结果在更弱的理论中依然成立，这些理论不支持Kleene代数的归纳公理。该结论表明，即使在简化条件下，相关形式系统的可判定性仍无法保证。

原文摘要 · Abstract (English)

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.

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。