摘要
自动定理证明一直是人工智能领域中最重要的问题之一,基于归结的方法是通过推出空子句的方法来判定子句集的可满足性.基于扩展规则的定理证明方法在一定意义上是和归结原理对偶的方法,是通过子句集能否推导出所有极大项组成的子句集来判定可满足性.通过对扩展规则的研究给出了半扩展规则的概念,并提出了基于半扩展规则的定理证明算法SER.然后分析及证明了该算法的正确性、完备性和复杂性.实验结果表明,算法SER的执行效率较基于归结的有向归结算法DR和基于扩展规则算法IER,NER有明显的提高.
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.
出处
《计算机研究与发展》
EI
CSCD
北大核心
2010年第9期1522-1529,共8页
Journal of Computer Research and Development
基金
国家自然科学基金重大项目(60496320
60496321)
国家自然科学基金项目(60973089
60773097
60873148)
吉林省科技发展计划基金项目(20060532
20080107)
欧盟合作项目(155776-EM-1-2009-1-IT-ERAMUNDUS-ECW-L12)
吉林大学研究生创新计划基金项目(20080242
20100026)
关键词
定理证明
命题逻辑
半扩展规则
可满足性问题
归结
theorem proving
propositional logic
semi-extension rule
satisfiability problem
resolution
