|
|||||
|
|
| 基于DTRC的形式自动证明平台及其应用 | |
| 引用本文： | 熊锋,李桂范,程明,冯速.基于DTRC的形式自动证明平台及其应用[J].海军工程大学学报,2004,16(5):60-64. |
| 作者姓名： | 熊锋 李桂范 程明 冯速 |
| 作者单位： | 1. 北京师范大学,信息科学学院,北京,100875 2. 黑龙江大学,数学科学学院,黑龙江,哈尔滨,150080 3. 北京师范大学,继续教育与教师培训学院,北京,100009 |
| 基金项目： | 国家自然科学基金资助项目(60273015) |
| 摘 要： | 动态项重写计算(DTRC)是项重写系统(TRS)的元计算模型,具有层次化结构和动态重写等特征,可应用于归纳定理的形式自动证明以及项重写系统弱终止性的形式自动证明等方面.文中介绍了一个基于DTRC的形式自动证明平台及其在TRS弱终止性自动证明上的应用. |
| 关 键 词： | 动态项重写计算 项重写系统 运行平台 形式自动证明 重写策略 |
| 文章编号： | 1009-3486(2004)05-0060-05 |
| 修稿时间： | 2004年5月10日 |
An automated formal proving platform based on dynamic term rewriting calculus and its application |
|
| XIONG Feng,LI Gui-fan,CHENG Ming,FENG Su.An automated formal proving platform based on dynamic term rewriting calculus and its application[J].Journal of Naval University of Engineering,2004,16(5):60-64. | |
| Authors: | XIONG Feng LI Gui-fan CHENG Ming FENG Su |
| Institution: | XIONG Feng~1,LI Gui-fan~2,CHENG Ming~3,FENG Su~1 |
| Abstract: | The dynamic term rewriting calculus is a formal computation model for meta-computation of term rewriting systems, which has characteristic features as the hierarchical declaration and dynamic rewriting, and is applied to the automated formal proving for the inductive theorems and weak termination of term rewriting systems. The paper describes an automated formal proving platform based on the dynamic term rewriting calculus and its application to the automated proving for the weak termination of term rewriting systems. |
| Keywords: | dynamic term rewriting calculus term rewriting systems computing platform automated formal proving rewriting strategy |
| 本文献已被 CNKI 万方数据 等数据库收录！ | |