命题模态归结的一种变型

A VARUNT OF PROPOSITIONAL MODAL RESOLUTION

本文给出了模态子句集的标准子句集概念，提出了一种基于标准子句集的模态归结方法的变型，称之为标准模态归结．证明了任意模态子句集恒假当且仅当存在从它的标准子句集出发，使用标准模态归结推出空子句的演绎．从而证明了对于不可满足标准予句集、标准模态归结是完备的．这种标准模态归结，推理规则简单、直观且容易实现．

This paper gives the notion of standard clause set of marked medal clause set.A method,called standard medal resolution t is presented,which is a variant of medal resolution method based on standard clause set.The soundness and completeness of standard medal resolution with respeCt to modal clause set is proved.