模态逻辑K、K_4系统Matrix证明方法中的可采纳替换

ADMISSIBLE SUBSTITUTION IN MATRIX METHOD FOR MODAL SYSTEMS K, K_4

Wallen的模态逻辑Matrix证明方法是在机器上较容易实现的一种模态逻辑自动推理方法.它将推理的难点转移到求可采纳替换中去,因而,可采纳替换的计算构成了模态逻辑Matrix证明方法的本质内容.本文讨论了模态逻辑K、K_4系统可采纳替换的存在性对多重性函数μ的依赖关系;指出了Wallen关于模态逻辑K、K_4系统的K-原子路径的若干结果和定义是不合适的,从而其某些结论是不正确的.

The modal Matrix method proposed by Wallen is an automated reasoning method which is easier to implement on computer for modal logics. But it translate the reasoning steps into computing admissible substitution, so the certral problem of modal Matrix method is how to compute the admissible substitution. Here, we discuss when the admissible substitution exist, and how it depend on the multiplicity u for modal systems K,K4,and then, we point out some results and definations of Wallen are unfit, and some conclusions are incorrect.