基于DTRC的形式自动证明平台及其应用  

An automated formal proving platform based on dynamicterm rewriting calculus and its application

作　　者：熊锋[1] 李桂范[2] 程明[3] 冯速[1] 

机构地区：[1]北京师范大学信息科学学院,北京100875 [2]黑龙江大学数学科学学院,黑龙江哈尔滨150080 [3]北京师范大学继续教育与教师培训学院,北京100009

出　　处：《海军工程大学学报》2004年第5期60-64,共5页Journal of Naval University of Engineering

基　　金：国家自然科学基金资助项目(60273015)

摘　　要：动态项重写计算(DTRC)是项重写系统(TRS)的元计算模型,具有层次化结构和动态重写等特征,可应用于归纳定理的形式自动证明以及项重写系统弱终止性的形式自动证明等方面.文中介绍了一个基于DTRC的形式自动证明平台及其在TRS弱终止性自动证明上的应用.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.

关 键 词：动态项重写计算 项重写系统 运行平台 形式自动证明 重写策略 

分 类 号：TP3[自动化与计算机技术—计算机科学与技术]