ISSN 1000-1239 CN 11-1777/TP

• 论文 • 上一篇    下一篇

基于半扩展规则的定理证明方法

张立明 欧阳丹彤 白洪涛   

  1. (吉林大学计算机科学与技术学院 长春 130012) (符号计算与知识工程教育部重点实验室(吉林大学) 长春 130012) (zhanglimingjlu@gmail.com)
  • 出版日期: 2010-09-15

Theorem Proving Algorithm Based on Semi-Extension Rule

Zhang Liming, Ouyang Dantong, and Bai Hongtao   

  1. (School of Computer Science and Technology, Jilin University, Changchun 130012) (Key Laboratory of Symbolic Computation and Knowledge Engineering (Jilin University), Ministry of Education, Changchun 130012)
  • Online: 2010-09-15

摘要: 自动定理证明一直是人工智能领域中最重要的问题之一,基于归结的方法是通过推出空子句的方法来判定子句集的可满足性.基于扩展规则的定理证明方法在一定意义上是和归结原理对偶的方法,是通过子句集能否推导出所有极大项组成的子句集来判定可满足性.通过对扩展规则的研究给出了半扩展规则的概念,并提出了基于半扩展规则的定理证明算法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.

Key words: theorem proving, propositional logic, semi-extension rule, satisfiability problem, resolution