LFD的有限模型性质与互模拟
计算机科学中的逻辑
2021-07-14 v1 逻辑
摘要
最近，Baltag和van Benthem arXiv:2103.14946 [cs.LO] 引入了一种新的可判定的功能依赖逻辑（LFD），具有局部依赖公式和依赖量词。该语言在依赖模型上解释，依赖模型是带有可用变量赋值集合（也称为团队）的一阶结构对。与依赖模型关联的团队可以看作是一个带标签的转移系统，在该系统上LFD成为一种模态逻辑，其中依赖量词成为模态词，局部依赖公式被视为特殊原子。在本文中，我们引入了适当的互模拟概念来刻画LFD（以及一些相关逻辑）作为一阶逻辑（FOL）的一个片段，并证明它等价于arXiv:2102.10368 [cs.LO]中提出的更标准路线的互模拟概念，但在互模拟检查方面更高效。我们的主要结果是LFD具有有限模型性质（FMP），通过Herwig关于扩展部分同构定理的新应用得到证明。
引用
@article{arxiv.2107.06042,
title = {Finite Model Property and Bisimulation for LFD},
author = {Raoul Koudijs},
journal= {arXiv preprint arXiv:2107.06042},
year = {2021}
}
备注
15 pages, submitted for GandALF 2021 conference