Cyclic proof theory breaks tradition by allowing certain infinite proofs: those that can be represented by a finite graph, while satisfying a soundness condition. We reconcile cyclic proofs with traditional finite proofs: we extend abstract cyclic proof systems with a well-founded induction principle, and transform any cyclic proof into a finite proof in the extended system. Moreover, this transformation preserves the structure of the cyclic proof. Our results leverage an annotated representation of cyclic proofs, which allows us to extract induction hypotheses and to determine their introduction order. The representation is essentially a reset proof with one key modification: names must be covered in a uniform way before a reset. This innovation allows us to handle cyclic proofs where the underlying inductive sort is non-linear. Our framework is general enough to cover recursive functions satisfying the size-change termination principle, which are viewed as cyclic proofs under the Curry-Howard correspondence.

翻译：循环证明理论打破了传统，允许某些无限证明：那些可以由有限图表示，同时满足可靠性条件的证明。我们将循环证明与传统有限证明相协调：通过引入良基归纳原则扩展抽象循环证明系统，并将任何循环证明转换为扩展系统中的有限证明。此外，该转换保持了循环证明的结构。我们的研究成果利用了循环证明的标注表示法，这使得我们能够提取归纳假设并确定其引入顺序。该表示本质上是一种重置证明，但有一个关键修改：在重置前必须以统一方式覆盖名称。这一创新使我们能够处理底层归纳类型为非线性的循环证明。我们的框架具有足够的通用性，能够涵盖满足大小变化终止原则的递归函数，这些函数在柯里-霍华德对应下被视为循环证明。