基于imom和ibohm启发式策略的扩展规则算法

基于扩展规则的方法是一种定理证明方法.在ier(improvedextensionrule)扩展规则算法的基础上,提出了imom(improvedmaximumoccurrencesonclausesofmaximumsize)和ibohm(improvedbohm)启发式策略,并将两种启发式策略用于ier算法中,有指导性地选择限定搜索空间的子句,设计并实现了算法imomh_ier和ibohmh_ier.实验结果表明,由于这两种启发式策略能够选择较为合适的搜索空间,可以尽快地判定出原问