This paper investigates the admissibility of the substitution rule in cyclic-proof systems. The substitution rule complicates theoretical case analysis and increases computational cost in proof search since every sequent can be a conclusion of an instance of the substitution rule; hence, admissibility is desirable on both fronts. While admissibility is often shown by local proof transformations in non-cyclic systems, such transformations may disrupt cyclic structure and do not readily apply. Prior remarks suggested that the substitution rule is likely nonadmissible in the cyclic-proof system CLKID^omega for first-order logic with inductive predicates. In this paper, we prove admissibility in CLKID^omega, assuming the presence of the cut rule. Our approach unfolds a cyclic proof into an infinitary form, lifts the substitution rules, and places back edges to construct a cyclic proof without the substitution rule. If we restrict substitutions to exclude function symbols, the result extends to a broader class of systems, including cut-free CLKID^omega and cyclic-proof systems for the separation logic.

翻译：本文研究循环证明系统中替换规则的可采纳性。替换规则使理论案例分析复杂化，并增加了证明搜索的计算成本，因为每个相继式都可能成为替换规则实例的结论；因此，该规则在理论和实践层面的可采纳性均具有重要价值。虽然在非循环系统中，可采纳性通常通过局部证明变换来证明，但此类变换可能破坏循环结构且难以直接应用。先前研究指出，在一阶逻辑带归纳谓词的循环证明系统CLKID^ω中，替换规则很可能不可采纳。本文证明在允许切规则的前提下，CLKID^ω中的替换规则具有可采纳性。我们的方法将循环证明展开为无穷形式，提升替换规则，并通过重建回边构造不含替换规则的循环证明。若将替换限制为不包含函数符号，该结果可推广至更广泛的系统类别，包括无切规则的CLKID^ω及分离逻辑的循环证明系统。