Tableau-Based Proving System for Medium Modal Logic MS_4
Nuaa Nanjing · Transaction of Nanjing University of Aeronautics and Astronautics · 1995
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.