The axiomatic translation principle for modal logic
The axiomatic translation principle for modal logic
复制标题
模态逻辑的公理翻译原理
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
U. Hustadt
中科院分区：
文献类型：
--
作者：
R. Schmidt;U. Hustadt
在本文中，我们提出了一个翻译原则，称为公理化翻译，用于将具有及物性、欧几里得性和功能等三角性质的背景理论的命题模态逻辑约简为一阶逻辑的可决片段。公理化翻译原则的目标是找到简化的理论，这些理论捕获了原始理论中的推理问题，但可以很容易地自动化，并且比标准翻译更容易被现有的（一阶）定理证明者处理。公理翻译的原理在概念上非常简单，几乎可以完全自动化。在合理的假设下，稳健性是自动的，一般的可决性结果可以陈述，并且很容易实现有序解决的终止。该方法的重要部分是证明完整性。我们证明了一些常见和不常见模态逻辑的完备性、可决性、模型生成、小模型性质和插值性质。我们还给出了一些一阶逻辑定理证明的实验结果，这是非常令人鼓舞的。
In this paper we present a translation principle, called the axiomatic translation, for reducing propositional modal logics with background theories, including triangular properties such as transitivity, Euclideanness and functionality, to decidable fragments of first-order logic. The goal of the axiomatic translation principle is to find simplified theories, which capture the inference problems in the original theory, but in a way that can be readily automated and is easier to deal with by existing (first-order) theorem provers than the standard translation. The principle of the axiomatic translation is conceptually very simple and can be almost completely automated. Soundness is automatic under reasonable assumptions, general decidability results can be stated and termination of ordered resolution is easily achieved. The non-trivial part of the approach is proving completeness. We prove results of completeness, decidability, model generation, the small model property and the interpolation property for a number of common and less common modal logics. We also present results of experiments with a number of first-order logic theorem provers which are very encouraging.