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代数类的协调性。所有结果均在Rocq证明助手中完全机械化实现，确保了正确性并支持插值式的有效计算。