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

被引：0

作者：

孙吉贵

刘叙华

机构：

[1] 吉林大学计算机科学系

来源：

模式识别与人工智能 | 1996年 / 9卷 / 03期

基金：

国家攀登计划;

关键词：

模态逻辑的自动推理; Matrix证明方法; 可采纳替换;

D O I：

暂无

中图分类号：

TP181 [自动推理、机器学习];

学科分类号：

摘要：

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

引用

页码：234 / 238

页数：5