主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公English
2020-2021年专刊出版计划 微信服务介绍 最新一期:2020年第10期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
张立明,欧阳丹彤,赵毅.半扩展规则下分解的定理证明方法.软件学报,2015,26(9):2250-2261
半扩展规则下分解的定理证明方法
Theorem Proving Decomposition Algorithm Based on Semi-Extension Rule
投稿时间:2014-04-12  
DOI:10.13328/j.cnki.jos.004734
中文关键词:  定理证明  命题逻辑  扩展规则  可满足性问题
英文关键词:theorem proving  propositional logic  extension rule  satisfiability problem
基金项目:国家自然科学基金(61133011, 61272208, 61402196, 61003101, 61170092); 吉林省科技发展计划(20101501, 20140520067JH); 中国博士后科学基金(2013M541302)
作者单位E-mail
张立明 吉林大学 计算机科学与技术学院, 吉林 长春 130012
符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 130012
吉林大学 电子科学与工程学院, 吉林 长春 130012 
 
欧阳丹彤 吉林大学 计算机科学与技术学院, 吉林 长春 130012
符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 130012 
ouyangdantong@163.com 
赵毅 吉林大学 电子科学与工程学院, 吉林 长春 130012  
摘要点击次数: 1840
全文下载次数: 1769
中文摘要:
      基于扩展规则的定理证明方法在一定意义上是与归结原理对偶的方法,通过子句集能否推导出所有极大项来判定可满足性.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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利