混合模态逻辑的有穷模型性研究

On the Finite Model Property of F usions of Modal Logics

本文研究了混合模态逻辑的有穷模型性问题,介绍了一种基于代数证明论的有穷模型性证明新方法,并用该方法证明了混合时态逻辑K4.t和模态逻辑S5的混合逻辑具有有穷模型性。因此可推导出混合时态逻辑K4.t和模态逻辑S5是可判定的。该结果被延伸到其他常见的时态逻辑与模态逻辑的混合,时态逻辑之间的混合和模态逻辑之间的混合,并得到它们的有穷模型性证明。

In this paper we study the finite model property of fusion of classical tense and modal logics. We introduce an algebraic proof theory method and prove the fusion of tense logic K4.t and modal logic S5 has the finite model property, which yields the decid-ability of this fusion logic. This result can be extended to some other fusions of normal modal and tense logics.