位置:成果数据库 > 期刊 > 期刊详情页
半扩展规则下分解的定理证明方法
  • ISSN号:1000-9825
  • 期刊名称:《软件学报》
  • 时间:0
  • 分类:TP181[自动化与计算机技术—控制科学与工程;自动化与计算机技术—控制理论与控制工程]
  • 作者机构:[1]吉林大学计算机科学与技术学院,吉林长春130012, [2]符号计算与知识工程教育部重点实验室(吉林大学),吉林长春130012, [3]吉林大学电子科学与工程学院,吉林长春130012
  • 相关基金:国家自然科学基金(61133011,61272208,61402196,61003101,61170092);吉林省科技发展计划(20101501,20140520067JH);中国博士后科学基金(2013M541302)
中文摘要:

基于扩展规则的定理证明方法在一定意义上是与归结原理对偶的方法,通过子句集能否推导出所有极大项来判定可满足性.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算法有明显的提高.

英文摘要:

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.

同期刊论文项目
期刊论文 99 会议论文 6
同项目期刊论文
期刊信息
  • 《软件学报》
  • 北大核心期刊(2011版)
  • 主管单位:中国科学院
  • 主办单位:中国科学院软件研究所 中国计算机学会
  • 主编:赵琛
  • 地址:北京8718信箱中国科学院软件研究所
  • 邮编:100190
  • 邮箱:jos@iscas.ac.cn
  • 电话:010-62562563
  • 国际标准刊号:ISSN:1000-9825
  • 国内统一刊号:ISSN:11-2560/TP
  • 邮发代号:82-367
  • 获奖情况:
  • 2001年入选中国期刊方阵“双百期刊”,2000年荣获中国科学院优秀科技期刊一等奖
  • 国内外数据库收录:
  • 俄罗斯文摘杂志,美国数学评论(网络版),波兰哥白尼索引,德国数学文摘,荷兰文摘与引文数据库,美国工程索引,美国剑桥科学文摘,英国科学文摘数据库,日本日本科学技术振兴机构数据库,中国中国科技核心期刊,中国北大核心期刊(2004版),中国北大核心期刊(2008版),中国北大核心期刊(2011版),中国北大核心期刊(2014版),中国北大核心期刊(2000版)
  • 被引量:54609