Rewriting Induction (RI) is a method to prove inductive theorems, originating from equational reasoning. By using Logically Constrained Simply-typed Term Rewriting Systems (LCSTRSs) as an intermediate language, rewriting induction becomes a tool for program verification, with inductive theorems taking the role of equivalence predicates. Soundness of RI depends on well-founded induction, and one of the core obstacles for obtaining a practically useful proof system is to find suitable well-founded orderings automatically. Using naive approaches, all induction hypotheses must be oriented within the well-founded ordering, which leads to very strong termination requirements. This, in turn, severely limits the proof capacity of RI. Here, we introduce Bounded RI: an adaption of RI for LCSTRSs where such termination requirements are minimized.

翻译：重写归纳法是一种源自等式推理的归纳定理证明方法。通过将逻辑约束简单类型项重写系统作为中间语言，重写归纳法成为程序验证的工具，其中归纳定理扮演等价谓词的角色。重写归纳法的可靠性依赖于良基归纳，而构建实用证明系统的核心障碍之一在于自动寻找合适的良基序。若采用朴素方法，所有归纳假设都必须在良基序中可定向，这导致极强的终止性要求，进而严重限制了重写归纳法的证明能力。本文提出有界重写归纳法：这是针对逻辑约束简单类型项重写系统的重写归纳法改进版本，其中此类终止性要求被最小化。