主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2019年第10期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
李爱中,黄厚宽,乔佩利.机器定理证明的反向归约方法.软件学报,1996,7(6):354-359
机器定理证明的反向归约方法
BACKWARD REDUCTION METHOD FOR AUTOMATED THEOREM PROVING
  修订日期:1995-03-30
DOI:
中文关键词:  自动定理证明  代数  递归  反向归约  数学归纳法  
英文关键词:Automated theorem proving  algebra  recursion  backward reduction  mathematical induction.
基金项目:本文研究得到国家自然科学基金资助.
作者单位
李爱中 北方交通大学计算机系,北京,100044 
黄厚宽 北方交通大学计算机系,北京,100044 
乔佩利 哈尔滨理工大学计算机系,哈尔滨,150040 
摘要点击次数: 2767
全文下载次数: 2803
中文摘要:
      基于代数和递归函数理论,本文定义了代数递归谓词.代数递归谓词是一类广泛的谓词.基于数学归纳法,作者给出了证明代数递归谓词永真性的反向归约方法及相应的算法Reduction.由于采用反向归约方式来完成定理证明,从根本上消除了正向组合式定理证明所产生的组合爆炸,因而极大地提高了定理证明的效率.
英文摘要:
      Based on algebra and recursive function theory, a key concept of algebraicrecursive predicates is defined in this paper. Based on mathematical induction, a backwardreduction method and its corresponding algorithm reduction are given for proving the universal truth of algebraic recursive predicates. Because the method is reduction based, theefficiency of theorem-proving is improved greatly.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

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