一种新的基于扩展规则的定理证明算法  

A Novel Theorem Proving Algorithm Based on Extension Rule

作　　者：孙吉贵[1,2] 李莹[1,2] 朱兴军[1,2] 吕帅[1,2] 

机构地区：[1]吉林大学计算机科学与技术学院,长春130012 [2]吉林大学符号计算与知识工程教育部重点实验室,长春130012

出　　处：《计算机研究与发展》2009年第1期9-14,共6页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(60773097);高等学校博士学科点基金项目(20050183065);吉林省青年科研基金项目(20080107)~~

摘　　要：基于扩展规则的定理证明方法是一种与归结方法互补的新的定理证明方法.首先通过对扩展规则的深入研究,给出了扩展规则的一个重要性质,设计并实现了该性质的判定算法.此外,从理论上分析及证明了该判定算法的时间和空间复杂性.基于此,提出了一种新的基于扩展规则的定理证明算法NER,将判定子句集可满足性问题转化为一系列文字集合的包含问题,而非计数问题.实验结果表明,算法NER的执行效率较原有扩展规则算法IER和基于归结的有向归结算法DR有明显提高,有些问题可以提高两个数量级.ATP （automated theorem proving） has always been one of the most advanced areas of computer science. The traditional idea used in ATP is to try to deduce the empty clause to check satisfiability, such as resolution based theorem proving, which is one of the most popular methods. Extension-rule-based theorem proving is a new resolution-based theorem proving method. After a deep research work on the extension rule, a brilliant property of the rule is obtained. In this paper, the property and an algorithm which is used to decide it are proposed firstly. In addition, the algorithm＇s time complexity and space complexity are analyzed and proved. Based on the above work, a novel extension rule based theorem proving algorithm called NER is proposed. The NER algorithm transforms the problem which decides whether a clause set is satisfiable to a series of problems deciding whether one literal set includes another one, while the original extension algorithm transforms them to problems counting the number of maximum terms that can be expended. A number of experiments show that the NER algorithm obviously outperforms both the original extension rule based algorithm ER and the directional resolution algorithm DR. Especially, it can be improved up to two orders of magnitude.

关 键 词：定理机器证明 命题逻辑 扩展规则 可满足性问题 归结 

分 类 号：TP181[自动化与计算机技术—控制理论与控制工程]