重写策略的终止：一种通用方法
摘要：基于对终止性质进行明确归纳的推理方法，我们提出了一种适用于策略重写的通用终止证明方法。基于ground terms的重写树通过交替应用缩小和抽象步骤生成证明树进行建模。归纳原理通过抽象机制应用，其中术语被用代表其任何正规形式的变量进行替换。归纳排序不是事先给定的，但是通过排序约束来定义，并在证明过程中逐步设置。抽象约束可用于控制著名容易发散的缩小机制。然后，通用方法被实例化为最内部、最外部和局部策略。
作者：Isabelle Gnaedig and Helene Kirchner
论文ID：cs/0507064
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23