欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
基于扩展规则的方法是一种定理证明方法．在IER（improved extension rule）扩展规则算法的基础上，提出了IMOM（improved maximum occurrences on clauses of maximum size）和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.
同期刊论文项目
同项目期刊论文
期刊信息
位置：