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

• 作者: 张立明 欧阳丹彤 赵毅
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 定理证明 命题逻辑 扩展规则 可满足性问题
• 年，卷（期）: 2015,（9）
• 所属期刊栏目: 模式识别与人工智能
• 页码范围: 2250-2261
• 页数: 12页
• 分类号: TP181
• 字数: 9995字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.004734

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	赵毅	吉林大学电子科学与工程学院	41	219	8.0	13.0