摘要
S5系统是一类知识表示能力和处理能力都较强的模态公理系统,它是认知逻辑、信念逻辑等非经典逻辑理论的基础。根据Kripke语义模型以及S5系统中部分公理,对命题模态逻辑S5公理系统的性质进行了较为深入的研究,并对S5系统中一类具有代表性的标准模态子句集的特性进行了分析,提出了一种基于扩展规则方法的命题模态逻辑推理算法(propositional modal clausal reasoning based on novel extension rule,PMCRNER)。针对朴素算法时间复杂度较高的问题,利用任务间潜在的关联性对算法同时进行了粗粒度与细粒度并行化,提出了并行算法PPMCRNER(parallel PMCRNER)理论框架,并且与基本算法进行了对比。实验结果表明,PPMCRNER算法在不可满足的子句集上的推理具有良好的加速比,为高时间复杂性的模态推理方法的进一步研究提供了一种可行方案。
S5 system is a special and important axiomatic system in propositional modal logic that has great ability of knowledge representation and processing, which is the basis of non-classical logics such as epistemic logic and belief logic etc. According to Kripke semantic model and part of the axioms in S5 system, this paper gives a more indepth research on the characteristics of propositional modal logic S5, and analyzes the features of a kind of representative formulae which is standard modal clauses, then proposes an NER-based algorithm called PMCRNER (propositional modal clausal reasoning based on novel extension rule) which is used to reason for standard modal clauses in propositional modal logic S5. In the view of high time complexity in simple algorithm, this paper uses the potential relevance between tasks to make the algorithm parallel in the degree of coarse-granularity and fine-granularity.This paper also gives the theoretical framework of PPMCRNER (parallel PMCRNER) and compares it with the basic algorithm. The experiments show that PPMCRNER has good speedup on unsatisfiable clause sets, and provides a feasible scheme for further research on the reasoning methods for modal formulae which are hard to solve.
作者
杨洋
李广力
张桐搏
刘磊
吕帅
YANG Yang;LI Guangli;ZHANG Tongbo;LIU Lei;LV Shuai(College of Computer Science and Technology, Jilin University, Changchun 130012, China;College of Mathematics, Jilin University, Changchun 130012, China;Key Laboratory of Symbolic Computation and Knowledge Engineering (Jilin University), Ministry of Education,Changchun 130012, China)
出处
《计算机科学与探索》
CSCD
北大核心
2016年第12期1783-1792,共10页
Journal of Frontiers of Computer Science and Technology
基金
国家自然科学基金Nos.61300049
61502197
61503044
高等学校博士学科点专项科研基金No.20120061120059~~
关键词
命题模态逻辑
S5公理系统
并行推理
扩展规则
propositional modal logic
S5 axiom system
parallel reasoning
extension rule