We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong L\"ob logic $\sf{iSL}$, an intuitionistic modal logic with a provability interpretation. A novel measure on sequents is used to prove both the termination of the naive backward proof search strategy, and the admissibility of cut in a syntactic and direct way, leading to a straightforward cut-elimination procedure. All proofs have been formalised in the interactive theorem prover Coq.

翻译：我们为直觉主义强Löb逻辑$\sf{iSL}$提供了一种新的矢列演算，该演算具有语法切割消去和强终止逆向证明搜索性质。$\sf{iSL}$是一种具有可证性解释的直觉主义模态逻辑。我们采用一种新的矢列测度，既证明了朴素逆向证明搜索策略的终止性，又以一种语法化且直接的方式证明了切割规则的可容许性，从而得到简洁的切割消去过程。所有证明均在交互式定理证明器Coq中完成形式化。