项重写系统弱基终止性的归纳证明

摘要：

This paper proposes a novel method for proving weakly ground termination in a restricted domain of a term rewriting system based on structural and cover set induction. For this prupose,we introduce the concepts of base set and set of ground terms defined recursively over base sets,which plays a crucial role in the inductive method. The method can be used for non-terminating,non-confluent and/or non-linear term rewriting systems,and have application in inductive equivalence testing and program verification.

关键词：Weakly ground termination、Induction、Term rewriting systems、Automated proving

所属期刊栏目：28

分类号：TP3(计算技术、计算机技术)

资助基金：国家自然科学基金19931020

在线出版日期：2004-01-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：105-108