一句话：将饱和证明器中基于循环检测的归纳证明方法抽象为子句集环，并厘清其与若干归纳理论的包含关系。
本文研究基于饱和式证明器中循环检测的一类自动归纳定理证明方法，旨在明确其逻辑强度。作者提出“子句集环”这一形式化概念，用以抽象子句集之间的循环依赖。首先证明子句集环形式化包含于 ∃₁ 归纳理论；随后通过给出三角数理论在开放归纳下的有限公理化，证明子句集环不包含于开放归纳理论，并猜想二者不可比较。最后把这些结果迁移到具体的自动归纳证明方法 n-clause calculus。
In this article we relate a family of methods for automated inductive theorem proving based on cycle detection in saturation-based provers to well-known theories of induction. To this end we introduce the notion of clause set cycles -- a formalism abstracting a certain type of cyclic dependency between clause sets. We first show that the formalism of clause set cycles is contained in the theory of $\exists_1$ induction. Secondly we consider the relation between clause set cycles and the theory of open induction. By providing a finite axiomatization of a theory of triangular numbers with open induction we show that the formalism of clause set cycles is not contained in the theory of open induction. Furthermore we conjecture that open induction and clause set cycles are incomparable. Finally, we transfer these results to a concrete method of automated inductive theorem proving called the n-clause calculus.