主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
李莹,孙吉贵,吴瑕,朱兴军.基于IMOM和IBOHM启发式策略的扩展规则算法.软件学报,2009,20(6):1521-1527
基于IMOM和IBOHM启发式策略的扩展规则算法
Extension Rule Algorithms Based on IMOM and IBOHM Heuristics Strategies
投稿时间:2007-11-05  修订日期:2008-07-02
DOI:
中文关键词:  定理机器证明  命题逻辑  扩展规则  启发式策略  归结
英文关键词:theorem proving  propositional logic  extension rule  heuristic strategy  resolution
基金项目:Supported by the National Natural Science Foundation of China under Grant No.60773097 (国家自然科学基金); the Young Scientific Research Foundation of JiLin Province of China under Grant No.20080107 (吉林省青年科研基金)
作者单位
李莹 吉林大学 计算机科学与技术学院,吉林 长春 130012
吉林大学 符号计算与知识工程教育部重点实验室,吉林 长春 130012 
孙吉贵 吉林大学 计算机科学与技术学院,吉林 长春 130012
吉林大学 符号计算与知识工程教育部重点实验室,吉林 长春 130012 
吴瑕 吉林大学 计算机科学与技术学院,吉林 长春 130012
吉林大学 符号计算与知识工程教育部重点实验室,吉林 长春 130012 
朱兴军 吉林大学 计算机科学与技术学院,吉林 长春 130012
吉林大学 符号计算与知识工程教育部重点实验室,吉林 长春 130012 
摘要点击次数: 4028
全文下载次数: 3746
中文摘要:
      基于扩展规则的方法是一种定理证明方法.在IER(improved extension rule)扩展规则算法的基础上,提出了IMOM(improved maximum occurrences on clauses of maximum size)和IBOHM(improved BOHM)启发式策略,并将两种启发式策略用于IER算法中,有指导性地选择限定搜索空间的子句,设计并实现了算法IMOMH_IER和IBOHMH_IER.实验结果表明,由于这两种启发式策略能够选择较为合适的搜索空间,可以尽快地判定出原问
英文摘要:
      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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利