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

An Inductive Proving Method for Weakly Ground Termination of Term Rewriting Systems

作　　者：冯速[1] 

机构地区：[1]北京师范大学计算机系,北京100875

出　　处：《计算机科学》2001年第7期105-108,共4页Computer Science

基　　金：国家自然科学基金(重点项目)(19931020)

摘　　要：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.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.

关 键 词：项重写系统 弱基终止性 归纳证明 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]