项重写系统等价性的归纳证明  

Equivalence Proving of Term Rewriting Systems by Induction

作　　者：冯速[1] 

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

出　　处：《计算机科学》2000年第8期5-7,共3页Computer Science

摘　　要：尽管学者们在计算机软件理论及相关数学理论方面做出了不懈的努力,但伴随着计算机硬件的高速发展而来的软件危机却日益严峻,其原因复杂多样。其中,主要原因之一是缺乏程序验证的方法和工具。程序设计的主要步骤有:描述问题、设计程序、实现程序及测试程序。需要注意的是,这里是测试程序的正确性而非证明程序的正确性。This paper proposes a simple but powerful method for proving the equivalence in a restricted domain of two term rewriting systems based on structural and cover set induction. Comparing with the well-studied inductionless induction methods and/or proof by transformation,the method is more natural and it is suitable for automated formal proving.

关 键 词：项重写系统 等价性 归纳证明 程序设计 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]