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

ADMISSIBLE SUBSTITUTION IN MATRIX METHOD FOR MODAL SYSTEMS K, K_4

作　　者：孙吉贵[1] 刘叙华[1] 

机构地区：[1]吉林大学计算机科学系,长春130023

出　　处：《模式识别与人工智能》1996年第3期234-238,共5页Pattern Recognition and Artificial Intelligence

基　　金：国家自然科学基金;863计划;国家攀登计划资助课题

摘　　要：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.

关 键 词：模态逻辑 Matrix证明方法 可采纳替换 类演算 

分 类 号：O141.13[理学—数学]