命题模态逻辑S5系统中并行推理方法

• 作者: 刘磊 吕帅 张桐搏 李广力 杨洋
• 来源期刊: 计算机科学与探索
• 学科: 工学
• 关键词: 命题模态逻辑 S5公理系统 并行推理 扩展规则
• 年，卷（期）: 2016,（12）
• 所属期刊栏目: 理论与算法
• 页码范围: 1783-1792
• 页数: 10页
• 分类号: TP181
• 字数: 8334字
• 语种: 中文
• DOI: 10.3778/j.issn.1673-9418.1509035

摘要

S5系统是一类知识表示能力和处理能力都较强的模态公理系统,它是认知逻辑、信念逻辑等非经典逻辑理论的基础.根据Kripke语义模型以及S5系统中部分公理,对命题模态逻辑S5公理系统的性质进行了较为深入的研究,并对S5系统中一类具有代表性的标准模态子句集的特性进行了分析,提出了一种基于扩展规则方法的命题模态逻辑推理算法(propositional modal clausal reasoning based on novel extension rule,PMCRNER).针对朴素算法时间复杂度较高的问题,利用任务间潜在的关联性对算法同时进行了粗粒度与细粒度并行化,提出了并行算法PPMCRNER(parallel PMCRNER)理论框架,并且与基本算法进行了对比.实验结果表明,PPMCRNER算法在不可满足的子句集上的推理具有良好的加速比,为高时间复杂性的模态推理方法的进一步研究提供了一种可行方案.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘磊	吉林大学计算机科学与技术学院	211	1231	18.0	25.0
2	杨洋	吉林大学计算机科学与技术学院	91	401	8.0	17.0
3	张桐搏	吉林大学计算机科学与技术学院	7	6	2.0	2.0
4	李广力	吉林大学计算机科学与技术学院	6	8	2.0	2.0