半扩展规则下分解的定理证明方法

基于扩展规则的定理证明方法在一定意义上是与归结原理对偶的方法,通过子句集能否推导出所有极大项来判定可满足性.ier(improvedextensionrule)算法是不完备的算法,在判定子句集子空间不可满足时,并不能判定子句集的满足性,算法还需重新调用er(extensionrule)算法,降低了算法的求解效率.通过对子句集的极大项空间的研究,给出了子句集的极大项空间分解后子空间的求解方法.通过对扩展规则的研究,给出了极大项部分空间可满足性判定方法pser(partialsemi-extensionrule).在ier算法判定子空间不可满足时,可以调用pser算法判定子空间对应的补空间的可满足性,从而得到子句集的可满足性,避免了不能判定极大项子空间可满足性时需重新调用er算法的缺点,使得ier算法更完备.在此基础上,还提出dpser(degreepartialsemi-extensionrule)定理证明方法.实验结果表明:所提出的dpser和ipser的执行效率较基于归结的有向归结算法dr、ier及ner算法有明显的提高.