Pitts' proof-theoretic technique for uniform interpolation, which generates uniform interpolants from terminating sequent calculi, has only been applied to logics on an intuitionistic basis through single-succedent sequent calculi. We adapt the technique to the intuitionistic multi-succedent setting by focusing on the intuitionistic modal logic KM. To do this, we design a novel multi-succedent sequent calculus for this logic which terminates, eliminates cut, and provides a decidability argument for KM. Then, we adapt Pitts' technique to our calculus to construct uniform interpolants for KM, while highlighting the hurdles we overcame. Finally, by (re)proving the algebraisability of KM, we deduce the coherence of the class of KM-algebras. All our results are fully mechanised in the Rocq proof assistant, ensuring correctness and enabling effective computation of interpolants.

翻译：匹茨基于证明论的一致插值技术，可从终止的矢列式演算生成一致插值项，该技术此前仅通过单后承矢列式演算应用于直觉主义基础的逻辑。我们通过聚焦直觉主义模态逻辑KM，将该技术适配至直觉主义多后承框架。为此，我们为KM设计了一种新颖的多后承矢列式演算，该演算具有终止性、可消去切规则，并提供了KM的可判定性证明。继而，我们将匹茨技术适配至所构造的演算，在攻克相应难点后为KM构建一致插值项。最后，通过（重新）证明KM的可代数化性，我们推导出KM代数簇的相干性。所有结果均在Rocq证明助手中完全机械化实现，确保了正确性并支持插值项的有效计算。