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

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.