机器定理证明的反向归约方法
BACKWARD REDUCTION METHOD FOR AUTOMATED THEOREM PROVING作者机构：北方交通大学计算机系哈尔滨理工大学计算机系
出 版 物：《软件学报》 (Journal of Software)
年 卷 期：1996年第7卷第6期
页 面：354-359页
核心收录：
学科分类：12[管理学] 1201[管理学-管理科学与工程(可授管理学、工学学位)] 081104[工学-模式识别与智能系统] 08[工学] 0835[工学-软件工程] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）]
基 金：国家自然科学基金
摘 要：基于代数和递归函数理论，本文定义了代数递归谓词．代数递归谓词是一类广泛的谓词．基于数学归纳法，作者给出了证明代数递归谓词永真性的反向归约方法及相应的算法Ｒｅｄｕｃｔｉｏｎ．由于采用反向归约方式来完成定理证明，从根本上消除了正向组合式定理证明所产生的组合爆炸，因而极大地提高了定理证明的效率．
维普期刊数据库
同方期刊数据库