摘要
动态项重写计算(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.
出处
《海军工程大学学报》
CAS
2004年第5期60-64,共5页
Journal of Naval University of Engineering
基金
国家自然科学基金资助项目(60273015)
关键词
动态项重写计算
项重写系统
运行平台
形式自动证明
重写策略
dynamic term rewriting calculus
term rewriting systems
computing platform
automated formal proving
rewriting strategy
