| 本文已被：浏览 6147次 下载 7759次 |
码上扫一扫！ |
|
|
| 基于IMOM和IBOHM启发式策略的扩展规则算法 |
|
李莹1,2, 孙吉贵1,2, 吴瑕1,2, 朱兴军1,2
|
|
1.吉林大学 计算机科学与技术学院,吉林 长春 130012;2.吉林大学 符号计算与知识工程教育部重点实验室,吉林 长春 130012
|
|
| 摘要: |
| 基于扩展规则的方法是一种定理证明方法.在IER(improved extension rule)扩展规则算法的基础上,提出了IMOM(improved maximum occurrences on clauses of maximum size)和IBOHM(improved BOHM)启发式策略,并将两种启发式策略用于IER算法中,有指导性地选择限定搜索空间的子句,设计并实现了算法IMOMH_IER和IBOHMH_IER.实验结果表明,由于这两种启发式策略能够选择较为合适的搜索空间,可以尽快地判定出原问 |
| 关键词: 定理机器证明 命题逻辑 扩展规则 启发式策略 归结 |
| DOI： |
| 分类号: |
| 基金项目:Supported by the National Natural Science Foundation of China under Grant No.60773097 (国家自然科学基金); the Young Scientific Research Foundation of JiLin Province of China under Grant No.20080107 (吉林省青年科研基金) |
|
| Extension Rule Algorithms Based on IMOM and IBOHM Heuristics Strategies |
|
LI Ying,SUN Ji-Gui,WU Xia,ZHU Xing-Jun
|
| Abstract: |
| Extension rule-based theorem proving is a splendid reasoning method. Based on the extension rule algorithm IER (improved extension rule), this paper proposes IMOM (improved maximum occurrences on clauses of maximum size) and IBOHM (improved BOHM) heuristic strategies in order to give guidance while choosing the clause that limits the search space. This paper applies these two heuristic strategies to the algorithm IER, designs and implements the algorithms IMOMH_IER and IBOHMH_IER. Since more appropriate search space can be obtained with these two heuristic strategies, the algorithms can decide whether the original question is satisfiable in a fraction of a second. Experimental results show that the speed of the algorithms is 10~200 times that of the existing algorithms DR (directional resolution) and IER. |
| Key words: theorem proving propositional logic extension rule heuristic strategy resolution |
