首页> 中文期刊> 《软件学报》 >半扩展规则下分解的定理证明方法

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

         

摘要

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

著录项

  • 来源
    《软件学报》 |2015年第9期|2250-2261|共12页
  • 作者

    张立明; 欧阳丹彤; 赵毅;

  • 作者单位

    吉林大学计算机科学与技术学院;

    吉林长春 130012;

    符号计算与知识工程教育部重点实验室(吉林大学);

    吉林长春 130012;

    吉林大学电子科学与工程学院;

    吉林长春 130012;

    吉林大学计算机科学与技术学院;

    吉林长春 130012;

    符号计算与知识工程教育部重点实验室(吉林大学);

    吉林长春 130012;

    吉林大学电子科学与工程学院;

    吉林长春 130012;

  • 原文格式 PDF
  • 正文语种 chi
  • 中图分类 自动推理、机器学习;
  • 关键词

    定理证明; 命题逻辑; 扩展规则; 可满足性问题;

相似文献

  • 中文文献
  • 外文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号