论文部分内容阅读
基于扩展规则的方法是一种定理证明方法．在IER（improved extension rule）扩展规则算法的基础上，提出了IMOM（improved maximum occurrences on clauses of maximum size）和IBOHM（improved BOHM）启发式策略，并将两种启发式策略用于IER算法中，有指导性地选择限定搜索空间的子句，设计并实现了算法IMOMH—IER和IBOHMH_IER．实验结果表明，由于这两种启发式策略能够选择较为合适的搜索空间，可以尽快地判定出原问