Term Rewriting Induction
Term Rewriting Induction
复制标题
术语重写归纳
DOI：
10.1007/3-540-52885-7_86
复制
发表时间：
1990
期刊：
影响因子：
--
通讯作者：
U. Reddy
中科院分区：
文献类型：
--
作者：
U. Reddy
提出了一种称为术语重写归纳的归纳方法，用于证明术语重写系统的属性。结果表明，基于 Knuth-Bendix 完成的归纳证明程序构造了术语重写归纳证明。迄今为止，人们普遍认为这些过程通过一致性来构造证明，并且不能被证明是归纳方法。我们的公式表明情况并非如此。从技术上讲，我们的结果超越了早期的结果，因为它独立于所涉及的重写系统的汇合或地面汇合。这解决了最近对该方法提出的主要批评之一。
An induction method called term rewriting induction is proposed for proving properties of term rewriting systems. It is shown that the Knuth-Bendix completion-based inductive proof procedures construct term rewriting induction proofs. It has been widely held heretofore that these procedures construct proofs by consistency, and cannot be justified as induction methods. Our formulation shows otherwise. Technically, our result goes beyond the earlier ones in that it is independent of the confluence or ground confluence of the rewrite systems involved. This addresses one of the major criticisms of the method raised in recent times.