Term rewriting induction

Abstract

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.