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

摘要：

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

关键词：定理证明、命题逻辑、扩展规则、可满足性问题

所属期刊栏目：26

分类号：TP181(自动化基础理论)

资助基金：国家自然科学基金61133011,61272208,61402196,61003101,61170092;吉林省科技发展计划20101501,20140520067JH;中国博士后科学基金2013M541302

在线出版日期：2016-08-19（万方平台首次上网日期，不代表论文的发表时间）

页数：共12页

页码：2250-2261