张立明 欧阳丹彤 白洪涛. 基于半扩展规则的定理证明方法[J]. 计算机研究与发展, 2010, 47(9): 1522-1529.
 引用本文: 张立明 欧阳丹彤 白洪涛. 基于半扩展规则的定理证明方法[J]. 计算机研究与发展, 2010, 47(9): 1522-1529.
Zhang Liming, Ouyang Dantong, and Bai Hongtao. Theorem Proving Algorithm Based on Semi-Extension Rule[J]. Journal of Computer Research and Development, 2010, 47(9): 1522-1529.
 Citation: Zhang Liming, Ouyang Dantong, and Bai Hongtao. Theorem Proving Algorithm Based on Semi-Extension Rule[J]. Journal of Computer Research and Development, 2010, 47(9): 1522-1529.

## Theorem Proving Algorithm Based on Semi-Extension Rule

• 摘要: 自动定理证明一直是人工智能领域中最重要的问题之一,基于归结的方法是通过推出空子句的方法来判定子句集的可满足性.基于扩展规则的定理证明方法在一定意义上是和归结原理对偶的方法,是通过子句集能否推导出所有极大项组成的子句集来判定可满足性.通过对扩展规则的研究给出了半扩展规则的概念,并提出了基于半扩展规则的定理证明算法SER.然后分析及证明了该算法的正确性、完备性和复杂性.实验结果表明,算法SER的执行效率较基于归结的有向归结算法DR和基于扩展规则算法IER，NER有明显的提高.

Abstract: The classical NP-complete problem of ATP (automated theorem proving) has seen much interest in not just the theoretical computer science community, but also in areas where practical solutions to this problem which enable significant practical applications. However, NP-completeness does not exclude the possibility of finding algorithms that are efficient enough for solving many interesting satisfiability instances. These instances arise from many diverse areas many practical problems in AI planning, circuit testing and verification for instance. ATP has always been one of the central concerns of AI, and resolution-based TP is to try to deduce the empty clause to check satisfiability. While the extension-rule-based TP proceeds inversely to resolution, which checks the satisfiability by deducing the set of clauses consisting of all the maximum terms. Scholars have investigated the extension-rule method. For example, Murray has applied the extension rule to the generation of the target language based on the knowledge compilation, and achieved good results. After a deep investigation on the extension rule, the concept of semi-extension rule is proposed. Based on the above work, a semi-extension-rule-based theorem proving algorithm so-called SER is present. Moreover, the approachs soundness, completeness and complexity are analyzed and proved. Finally, results show that the efficiency of algorithm SER is highly improved, which obviously outperforms both the directional resolution algorithm DR and the extension-rule-based algorithms IER and NER.

/

• 分享
• 用微信扫码二维码

分享至好友和朋友圈