HoCHC：一个反驳完全且语义不变的高阶逻辑模理论系统
计算机科学中的逻辑
2021-06-22 v2
摘要
我们提出了一个用于高阶约束 Horn 子句 (HoCHC)——一种高阶逻辑模理论系统——的简单归结证明系统，并证明了其关于标准语义的可靠性与反驳完全性。作为推论，我们获得了 HoCHC 在半可判定背景理论下的紧致性定理与半可判定性，并证明了 HoCHC 满足典范模型性质。此外，一个众所周知的从高阶逻辑到一阶逻辑的翻译的变体被证明对于标准语义下的 HoCHC 是可靠且完全的。我们说明了如何将（一阶逻辑模理论的）片段的可判定性结果转移到我们的高阶设定中，以受限形式的线性整数算术模下的 Bernays-Schonfinkel-Ramsey 片段作为例子。
引用
@article{arxiv.1902.10396,
title = {HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories},
author = {C. -H. Luke Ong and Dominik Wagner},
journal= {arXiv preprint arXiv:1902.10396},
year = {2021}
}