存在性二阶逻辑及具有团队语义的逻辑的并闭片段
摘要：存在第二阶逻辑和具有团队语义的逻辑的并闭分片的句法特征。由于并闭性是一种语义的不可判定属性，我们引入的正规形式使得能够处理并提供对这个分片的更好理解。我们还引入了互斥关系游戏，结果证明它们恰好是相应的模型检查游戏。这些游戏不仅本身有趣，而且也是在语义和句法分片之间建立桥梁的关键因素。在具有团队语义的逻辑层面上，我们还将互斥关系逻辑的限制引入，以捕捉并闭分片。此外，我们定义了基于团队的原子，当将其添加到一阶逻辑中时，也可以精确地捕获存在第二阶逻辑的并闭分片，这回答了Galliani和Hella的一个悬而未决问题。
作者：Matthias Hoelzel and Richard Wilke
论文ID：1910.06057
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22