###
DOI:
Journal of Software:2009.20(6):1521-1527

基于IMOM和IBOHM启发式策略的扩展规则算法
李莹,孙吉贵,吴瑕,朱兴军
(吉林大学 计算机科学与技术学院,吉林 长春 130012;吉林大学 符号计算与知识工程教育部重点实验室,吉林 长春 130012)
Extension Rule Algorithms Based on IMOM and IBOHM Heuristics Strategies
LI Ying,SUN Ji-Gui,WU Xia,ZHU Xing-Jun
()
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 3669   Download 3489
Received:November 05, 2007    Revised:July 02, 2008
> 中文摘要: 基于扩展规则的方法是一种定理证明方法.在IER(improved extension rule)扩展规则算法的基础上,提出了IMOM(improved maximum occurrences on clauses of maximum size)和IBOHM(improved BOHM)启发式策略,并将两种启发式策略用于IER算法中,有指导性地选择限定搜索空间的子句,设计并实现了算法IMOMH_IER和IBOHMH_IER.实验结果表明,由于这两种启发式策略能够选择较为合适的搜索空间,可以尽快地判定出原问
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.
文章编号:     中图分类号:    文献标志码:
基金项目: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 (吉林省青年科研基金) 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 (吉林省青年科研基金)
Foundation items:
Reference text:

李莹,孙吉贵,吴瑕,朱兴军.基于IMOM和IBOHM启发式策略的扩展规则算法.软件学报,2009,20(6):1521-1527

LI Ying,SUN Ji-Gui,WU Xia,ZHU Xing-Jun.Extension Rule Algorithms Based on IMOM and IBOHM Heuristics Strategies.Journal of Software,2009,20(6):1521-1527