【摘要】 基于扩展规则的定理证明方法是一种与归结方法互补的新的定理证明方法.首先通过对扩展规则的深入研究,给出了扩展规则的一个重要性质,设计并实现了该性质的判定算法.此外,从理论上分析及证明了该判定算法的时间和空间复杂性.基于此,提出了一种新的基于扩展规则的定理证明算法NER,将判定子句集可满足性问题转化为一系列文字集合的包含问题,而非计数问题.实验结果表明,算法NER的执行效率较原有扩展规则算法IER和基于归结的有向归结算法DR有明显提高,有些问题可以提高两个数量级.更多还原

【Abstract】 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.更多还原