###
Journal of Software:2015.26(9):2250-2261

半扩展规则下分解的定理证明方法
张立明,欧阳丹彤,赵毅
(吉林大学 计算机科学与技术学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 130012;吉林大学 电子科学与工程学院, 吉林 长春 130012)
Theorem Proving Decomposition Algorithm Based on Semi-Extension Rule
ZHANG Li-Ming,OUYANG Dan-Tong,Zhao Yi
(College of Computer Science and Technology, Jilin University, Changchun 130012, China;Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education (Jilin University), Changchun 130012, China;College of Electronic Science &)
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 1431   Download 1479
Received:April 12, 2014    
> 中文摘要: 基于扩展规则的定理证明方法在一定意义上是与归结原理对偶的方法,通过子句集能否推导出所有极大项来判定可满足性.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算法有明显的提高.
Abstract:The extension rule based theorem proving methods are inverse methods to resolution in a sense that they check the satisfiability by determining whether all the maximum terms of the clause set can be deduced. IER (improved extension rule) algorithm is incomplete as it cannot determine the satisfiability of the clause set when the subspace of the clause set is unsatisfiable. In this condition, calling ER (extension rule) algorithms is still needed. After a thorough investigation on the maximum terms space of the clause set, this paper develops a decomposition method for decomposing the maximum terms space of the clause set. The study on extension rule also results in the PSER (partial semi-extension rule) algorithm for determining the satisfiability of a partial space of the maximum terms. When the IER determines the subspace is unsatisfiable, PSER can be used to determine the satisfiability of the complementary space, thereby, the satisfiability of the clause set can be obtained. Based on the above progress, this paper further introduces DPSER (degree partial semi-extension rule) theorem proving method. Results show that the proposed DPSER and IPSER outperform both the directional resolution algorithm DR and the extension rule based algorithms IER and NER.
文章编号:     中图分类号:    文献标志码:
基金项目:国家自然科学基金(61133011, 61272208, 61402196, 61003101, 61170092); 吉林省科技发展计划(20101501, 20140520067JH); 中国博士后科学基金(2013M541302) 国家自然科学基金(61133011, 61272208, 61402196, 61003101, 61170092); 吉林省科技发展计划(20101501, 20140520067JH); 中国博士后科学基金(2013M541302)
Foundation items:
Reference text:

张立明,欧阳丹彤,赵毅.半扩展规则下分解的定理证明方法.软件学报,2015,26(9):2250-2261

ZHANG Li-Ming,OUYANG Dan-Tong,Zhao Yi.Theorem Proving Decomposition Algorithm Based on Semi-Extension Rule.Journal of Software,2015,26(9):2250-2261