中介模态逻辑MS_4的表推演系统

Tableau-Based Proving System for Medium Modal Logic MS_4

中介逻辑是一个新的逻辑系统，该系统的创立有明显的哲学背景，自创立后得到了很大的发展。在数理逻辑以及计算机科学领域已发展了中介模态逻辑以及ＭＩＬＬ等中介程序计设语言，但对作为程序计设语言之逻辑基础之一的中介模态逻辑的自动推理理论与实现的研究还很不够。本文系统地讨论中介模态逻辑ＭＳ４的自动定理证明理论，构造了中介模态逻辑ＭＳ４的表推演系统。由于该系统采用＂与或树＂的表达方法，因而不产生＂遗忘问题＂；又由于设置的μ＇扩展规则有效地限制了＂秩＂的递增次数，从而保证了该系统的完备性。本文第一部分给出了中介模态逻辑ＭＳ４的表推演系统及一个应用实例，第二部分证明了该系统的可靠性与完备性定理。

Medium logic system is a new logic system. The creation of this system has a strong philosophic background,so it is rapidly developed. In the fields of mathematical logic and computer science this system is applied to the medium modal logic and the base of MILL,a medium language of program. But the study of the theories and implementation of the proving system of the medium modal logic is not yet wide and deep enough. In this paper, the theories of automatic proof of the medium modal logic MS4 are studied systematically and the tableau-based proving system of the medium modal logic MS4 is presented. The method of using AND/OR tree is applied to the system so it does not lead up to the problem of neligence.Similarly, the system is complete since the rule μ' in the system effectively limits the increase of the rank of a set of formulas. In the first part of this paper,the tableau-based proving system for the medium modal logic MS4 is presented together with an example. In the second part, it is proved that the system is sound and complete.