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

摘要：

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

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

所属期刊栏目：10

分类号：TP181(自动化基础理论)

资助基金：The National Natural Science Foundation of China under Grant Nos.61300049,61502197,61503044;the Specialized Research Fund for the Doctoral Program of Higher Education of China under Grant No.20120061120059

在线出版日期：2017-02-24（万方平台首次上网日期，不代表论文的发表时间）

页数：共10页

页码：1783-1792