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

Abstract: 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 in-depth 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.

Key words: propositional modal logic, S5 axiom system, parallel reasoning, extension rule