我的阅读状态 （保存写回仓库，全设备同步；首次保存需输入访问令牌）

AI 速览

一句话：证明剩余 Kleene 格（动作格）的（不）等式理论不可判定，解决了长期开放问题。

本文研究剩余 Kleene 格（又称动作格）的逻辑，即其（不）等式理论的可判定性。此前该问题由 Kozen、Jipsen 和 Buszkowski 留下开放。作者证明了该（不）等式理论是算法不可判定的：不存在算法能判定任意动作格（不）等式是否成立。因此相应逻辑的有效性判定问题也不可判定。该结果关闭了一个长期开放问题，并给出动作逻辑、Kleene 代数及剩余格相关系统判定边界的一个强否定结论。

问题

剩余 Kleene 格（动作格）的（不）等式理论是否可判定，这是 Kozen、Jipsen 与 Buszkowski 留下的开放问题。

方法

论文给出动作格（不）等式理论的算法不可判定性证明。

评估

以理论证明方式确立不可判定性结果，并据此回答上述开放问题。

链接与引用

DOI 原文 ·

@inproceedings{paperbot5015,
  title = {The Logic of Action Lattices is Undecidable},
  author = {Stepan Kuznetsov},
  booktitle = {LICS},
  year = {2019},
  doi = {10.1109/lics.2019.8785659}
}