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

摘要

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