一句话：提出 Cut-Restriction，将任意切割限制为解析切割，在无法切消时恢复子公式性质并统一已有结果。
切消是证明论的基石，但多数非经典逻辑的相继式演算并不满足切消。实际应用真正依赖的往往是其推论——子公式性质。为此，作者引入 Cut-Restriction：当无法完全消去切割时，将任意切割限制为解析切割。该过程适用于所有满足语言无关且易于检查条件的相继式演算，其设计改编自经典切消算法。结果表明，该框架以统一方式涵盖已有解析切割结果，包含 Gentzen 的切消作为特例，并建立新的解析切割性质。
Cut-elimination is the bedrock of proof theory with a multitude of applications from computational interpretations to proof analysis. It is also the starting point for important meta-theoretical investigations into decidability, complexity, disjunction property, interpolation, and more. Unfortunately cut-elimination does not hold for the sequent calculi of most non-classical logics. It is well-known that the key to applications is the subformula property (a typical consequence of cut-elimination) rather than cut-elimination itself. With this in mind, we introduce cut-restriction, a procedure to restrict arbitrary cuts to analytic cuts (when elimination is not possible). The algorithm applies to all sequent calculi satisfying language-independent and simple-to-check conditions, and it is obtained by adapting age-old cut-elimination. Our work encompasses existing results in a uniform way, subsumes Gentzen’s cut-elimination, and establishes new analytic cut properties.