模态逻辑中算法对应性与完备性. I. 核心算法 SQEMA
计算机科学中的逻辑
2017-01-11 v4
摘要
模态公式用于表达 Kripke 框架上的一元谓词逻辑属性，但在许多重要情况下，这些属性具有一阶等价形式。计算此类等价形式对于逻辑和计算目的都很重要。另一方面，模态公式的规范性也很重要，因为它意味着以规范公式公理化的逻辑具有框架完备性。计算模态公式的一阶等价形式等价于消除二阶量词。已 developed 两种用于二阶量词消除的方法：SCAN 基于约束求解，DLS 基于阿克曼的逻辑等价原理。本文介绍一种新算法 SQEMA，用于计算一阶等价形式（采用模态版阿克曼引理），并且还能证明模态公式的规范性。与 SCAN 和 DLS 不同，SQEMA 直接作用用于模态公式，从而避免 Skolem 化及随后的不可 Skolem 化问题。我们给出核心算法并以示例进行说明。随后我们证明了其正确性以及所有算法成功处理的公式的规范性。我们指出，SQEMA 不仅适用于所有 Sahlqvist 公式，也适用于我们前期论文中引入的更大类的归纳公式。因此，我们发展了一种纯粹的算法方法，用于在模态逻辑中证明规范完备性，特别是确立了目前最为一般的完备性结果之一。
引用
@article{arxiv.cs/0602024,
title = {Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA},
author = {Willem Conradie and Valentin Goranko and Dimiter Vakarelov},
journal= {arXiv preprint arXiv:cs/0602024},
year = {2017}
}
备注
26 pages, no figures, to appear in the Logical Methods in Computer Science