摘要
基于扩展规则的方法是一种定理证明方法.在IER(improved extension rule)扩展规则算法的基础上,提出了IMOM(improved maximum occurrences on clauses of maximumsize)和IBOHM(improved BOHM)启发式策略,并将两种启发式策略用于IER算法中,有指导性地选择限定搜索空间的子句,设计并实现了算法IMOMH_IER和IBOHMH_IER.实验结果表明,由于这两种启发式策略能够选择较为合适的搜索空间,可以尽快地判定出原问题是否可满足,故其速度平均能够达到原有算法DR(directional resolution)和IER的10～200倍.
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.
出处
《软件学报》
EI
CSCD
北大核心
2009年第6期1521-1527,共7页
Journal of Software
基金
国家自然科学基金No.60773097
吉林省青年科研基金No.20080107~~
关键词
定理机器证明
命题逻辑
扩展规则
启发式策略
归结
theorem proving
propositional logic
extension rule
heuristic strategy
resolution
