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

来源：计算机科学与探索杂志2016年第12期北京时间：

作者：杨洋，李广力，张桐搏，刘磊，吕帅

单位：1. 吉林大学 计算机科学与技术学院，长春 1300122. 吉林大学 数学学院，长春 1300123. 符号计算与知识工程教育部重点实验室（吉林大学），长春 130012

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

关键词：命题模态逻辑,S5公理系统,并行推理,扩展规则