%0 Journal Article
%T 基于imom和ibohm启发式策略的扩展规则算法
%A 李莹？
%A 孙吉贵？
%A 吴瑕？
%A 朱兴军？
%J 软件学报
%P 1521-1527
%D 2009
%X 基于扩展规则的方法是一种定理证明方法.在ier(improvedextensionrule)扩展规则算法的基础上,提出了imom(improvedmaximumoccurrencesonclausesofmaximumsize)和ibohm(improvedbohm)启发式策略,并将两种启发式策略用于ier算法中,有指导性地选择限定搜索空间的子句,设计并实现了算法imomh_ier和ibohmh_ier.实验结果表明,由于这两种启发式策略能够选择较为合适的搜索空间,可以尽快地判定出原问
%K 定理机器证明
%K 命题逻辑
%K 扩展规则
%K 启发式策略
%K 归结
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=3420&flag=1