一种新的模态归结

A NEW STRATEGY OF MODAL RESOLUTION

本文首先给出了一种标准子句的定义，在其基础上定义了命题模态逻辑系统Ｓ５的子句集的可归结形式．证明了任意模态Ｓ５子句集不可满足的充要条件为在其可归结形式上可归结出空子句．

This paper gives the concept of standard clauses set and defines resolvable form of a clauses set. The soundness and completeness of modal resolution onresolvable form with respect to propositional modal logic system S5 is proved.