论文部分内容阅读
基于代数和递归函数理论，本文定义了代数递归谓词，代数递归谓词是一类广泛的谓词，基平均数学归纳法，作者给出了证明代数递归谓词永真性的反向归约方法及相应的算法Ｒｅｄｕｃｔｉｏｎ。由于采用反向归约方式来完成定理证明，从根本上消除了正向组合式定理证明了所产生的组合爆炸，因而极大地提高了定理证明的效率。
机器定理证明的反向归约方法
【摘 要】
：
基于代数和递归函数理论，本文定义了代数递归谓词，代数递归谓词是一类广泛的谓词，基平均数学归纳法，作者给出了证明代数递归谓词永真性的反向归约方法及相应的算法Ｒｅｄｕｃｔｉｏｎ。由于采用反向
【机 构】
：
北方交通大学计算机系,哈尔滨理工大学计算机系
【出 处】
：
软件学报
【发表日期】
：
1996年6期
其他文献
随着我国素质教育改革发展进程的不断加快，当前初中教育的主流仍然是应试教育模式，而初中德育，对青少年学生个体的生命体验与内在精神关注不够，德育的痕迹过深，德育活动的功利色彩
北京市东郊粮食交易市场4月底这期粮油成交量比上期有明显增加,尤其是大米成交十分活跃。总成交量797吨,总成交金额 216.9万吨。成交品种有:粳米、富强粉。 粳米:成交量617.1
实施组织变革是高职院校服务地方经济社会发展、推进教育教学改革、提升办学治校能力的必然选择。由中专学校合并升格的X校,从经济、社会、政策等外部因素和组织、个体、文化
本文介绍归纳法推理系统的核心－－归纳法模式的自动生成程序，该程序从递归函数定义出发，自动生成归纳法模板；从待证定理出发，借助归纳法模板，自动生成归纳法模式和归纳法公式，该系统已
《狂鼓史》中被誉为“神来之笔”的“乌悲词”可以说是“曼倩诙谐不是耍”的重要表现。《狂鼓史》中三段“乌悲词”,其“曼倩诙谐”是表,其“不是耍”的真意是里。通过对“乌
美国经济学家保罗·罗默的新增长理论是一种对长期经济增长进行预测的理论。传统的经济理论仅考虑生产中的两个因素:资本和劳动力,而它则将第三种因素——技术考虑进去。