具有路径上的n元关系的模态逻辑：共降凡子语义和表达能力
摘要：游戏共单子为有限模型论中的比较游戏提供了范畴语义，从而为一系列逻辑提供了抽象的等价性描述，每种逻辑通过特定的共单子选择进行捕捉。然而，像CoreDataXPath这样的数据感知逻辑呈现了复杂的双模拟概念，这与直接的共单子编码相悖。在这项工作中，我们通过引入模态逻辑的一种广义化来开始对数据感知逻辑的共单子处理，该广义化允许任意元数的关系符号作为语法的原子，我们称之为路径谓词模态逻辑(PPML)。我们以一种对已经研究的限制版本的CoreDataXPath，即DataGL的视角变化而得到这种逻辑，并证明了对于特定的签名选择，PPML可以恢复DataGL。我们认为这种视角变化允许捕捉和设计新的数据感知逻辑。另一方面，PPML在于其本质的动机是扩展模态逻辑以便于对更一般的模型进行谓词化。我们为PPML定义了仿真和双模拟游戏，并证明了一个Hennessy-Milner型定理，然后定义了PPML共单子并证明了它捕捉了这些游戏，这是文献中类似结果的扩展。与以往的研究不同的是，我们明确证明了我们的共单子满足树类别和树覆盖的公理。利用共单子机制，我们立即得到了PPML的树模型属性。最后，我们定义了一种从关系结构到Kripke结构的翻译函子，并利用其性质证明了一系列从PPML问题到基本模态逻辑问题的多项式时间归约。我们的结果明确说明了以何种方式PPML让我们通过模态镜头来观察一般的关系结构。
作者：Santiago Figueira, Gabriel Goren Roig
论文ID：2307.09679
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-20