| 一种新的基于扩展规则的定理证明算法 |
| |
| 引用本文： | 孙吉贵,李莹,朱兴军,吕帅.一种新的基于扩展规则的定理证明算法[J].计算机研究与发展,2009,46(1). |
| |
| 作者姓名： | 孙吉贵 李莹 朱兴军 吕帅 |
| |
| 作者单位： | 1. 吉林大学计算机科学与技术学院,长春,130012
2. 吉林大学符号计算与知识工程教育部重点实验室,长春,130012 |
| |
| 基金项目： | 国家自然科学基金，高等学校博士学科点基金，吉林省青年科研基金 |
| |
| 摘 要： | 基于扩展规则的定理证明方法是一种与归结方法互补的新的定理证明方法,首先通过对扩展规则的深入研究,给出了扩展规则的一个重要性质,设计并实现了该性质的判定算法.此外,从理论上分析及证明了该判定算法的时问和空间复杂性.基于此,提出了一种新的基于扩展规则的定理证明算法NER,将判定子句集可满足性问题转化为一系列文字集合的包含问题,而非计数问题.实验结果表明,算法NER的执行效率较原有扩展规则算法IER和基于归结的有向归结算法DR有明显提高,有些问题可以提高两个数量级.
|
| 关 键 词： | 定理机器证明 命题逻辑 扩展规则 可满足性问题 归结 |
A Novel Theorem Proving Algorithm Based on Extension Rule |
| |
| Sun Jigui,Li Ying,Zhu Xingjun,Lü Shuai.A Novel Theorem Proving Algorithm Based on Extension Rule[J].Journal of Computer Research and Development,2009,46(1). |
| |
| Authors: | Sun Jigui Li Ying Zhu Xingjun Lü Shuai |
| |
| Affiliation: | College of Computer Science and Technology;Jilin University;Changchun 130012;Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education;Changchun 130012 |
| |
| 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 t... |
| |
| Keywords: | theorem proving propositional logic extension rule satisfiability problem resolution |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
