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 including decidability, complexity, disjunction property, and interpolation. 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, and establishes novel analytic subformula properties.

翻译：分割消去是证明论的基石，具有从计算解释到证明分析的多重应用。它也是包括可判定性、复杂性、析取性质和插值性等重要元理论研究的起点。遗憾的是，对于大多数非经典逻辑的相继式演算而言，分割消去并不成立。众所周知，应用的关键在于子公式性质（分割消去的典型结果）而非分割消去本身。基于这一认识，我们引入分割-限制过程，将任意分割限制为分析性分割（当消去不可行时）。该算法适用于所有满足语言无关且易于检验条件的相继式演算，并通过改造经典分割消去方法实现。我们的工作以统一方式涵盖现有成果，并建立了新颖的分析性子公式性质。