重写策略的终止性：一种通用方法
计算机科学中的逻辑
2007-05-23 v1
摘要
我们提出一种基于终止性质显式归纳的、用于策略下重写的通用终止证明方法。基项上的重写树由证明树建模，证明树通过交替应用窄化（narrowing）和抽象步骤生成。归纳原理通过抽象机制应用，其中项被替换为表示其任意正规形式的变量。归纳序不是先验给定的，而是由序约束定义，在证明过程中增量式地设定。抽象约束可用于控制窄化机制，众所周知后者容易发散。然后将该通用方法实例化为最内、最外和局部策略。
引用
@article{arxiv.cs/0507064,
title = {Termination of rewriting strategies: a generic approach},
author = {Isabelle Gnaedig and Helene Kirchner},
journal= {arXiv preprint arXiv:cs/0507064},
year = {2007}
}
备注
49 pages