任意公告逻辑中具有共同知识的可满足性是$Σ^1_1$-难度
摘要：任意人公告逻辑与共同知识(APALC)是公告逻辑的一个扩展，具有共同知识模态和关于公告的量化器。我们展示了APALC在S5模型上的满足性问题，以及另外两个相关逻辑的满足性问题，都是Σ1_1-hard难题。这意味着APALC的有效性和可满足公式都不是可递归枚举的。反过来，这意味着APALC不是有限公理化的。
作者：Rustam Galimullin, Louwe B. Kuijer
论文ID：2307.05060
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-12