模态逻辑系统S5中的范式定理及其在知识系统中的应用

Normal form theorem in modal logic system S5 and its application to knowledge base theory

研究了模态逻辑系统S5中的析(合)取范式定理的归纳证明,给出了在S5中用深度至多等于1的最简模态公式通过析取与合取运算表示含有多重模态词的公式的方法.作为范式定理的应用,讨论了知识库中的一个基本问题,证明了知识库能够回答KB命题式问题的充要条件是该知识库能够回答相关的非模态命题及其否定命题的问题.

Disjunction （Conjunction） normal form theorem in the modal logic system S5 is inductively proved, which can be used for representing complex modal formulas by means of conjunction and disjunction of simplest modal formulas with depth at most 1 in the system S5. As application, it is proved that a knowledge base could answer KB-queries if and only if it could answer queries of nonmodal propositions and their negations, which is a basic problem on knowledge base.