基于IMOM和IBOHM启发式策略的扩展规则算法

• 作者: 吴瑕 孙吉贵 朱兴军 李莹
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 定理机器证明 命题逻辑 扩展规则 启发式策略 归结
• 年，卷（期）: 2009,（6）
• 所属期刊栏目: 模式识虽与人工智能
• 页码范围: 1521-1527
• 页数: 7页
• 分类号: TP181
• 字数: 4478字
• 语种: 中文
• DOI: 10.3724/SP.J.1001.2009.03420

摘要

基于扩展规则的方法是一种定理证明方法.在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倍.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	孙吉贵	吉林大学计算机科学与技术学院	134	2984	21.0	52.0
5	李莹	吉林大学计算机科学与技术学院	48	236	10.0	14.0
9	吴瑕	吉林大学计算机科学与技术学院	4	15	2.0	3.0