| 《计算机学报》文章摘要 全文下载 | |
| 文章题目 | 标记模态归结的推广 |
| 作者 | 孙吉贵 刘瑞胜 陈 荣 |
| 作者单位 | (吉林大学计算机科学系 长春 130023) (吉林大学符号计算与知识工程开放实验室 长春 130023) |
| 发表年份 | 1999 |
| 发表月份 | 2期 （页码：113—119) |
| 文章摘要 | 本文将作者提出的高效的命题模态D逻辑的标记模态归结方法推广到了命题模态逻辑K,K4,D4,T,S4系统,建立了上述命题模态逻辑的标记归结形式系统MRK,MRK4,MRD4,MRT,MRS4.并用转换子句模式的方法,借助于标记模态归结对命题模态D逻辑的可靠性结果,证明了标记模态归结系统MRK,MRK4, MRD4,MRT,MRS4分别关于命题模态逻辑K,K4,D4,T,S4的可靠性.进而得到了它们的完备性. 关键词 模态逻辑,模态推理,标记模态归结. |