Pitts 与直觉主义多后承：KM 的均匀插值
Pitts and Intuitionistic Multi-Succedent: Uniform Interpolation for KM
AI总结：
将 Pitts 的均匀插值证明论技术扩展到直觉主义多后承设定，为直觉主义模态逻辑 KM 设计终止的多后承相继演算并构造均匀插值，同时证明 KM-代数类的连贯性。
摘要：
Pitts 用于均匀插值的证明论技术，该技术从终止的相继演算生成均匀插值，此前仅通过单后承相继演算应用于直觉主义基础的逻辑。我们通过聚焦于直觉主义模态逻辑 KM，将该技术适应到直觉主义多后承设定。为此，我们为此逻辑设计了一个新颖的多后承相继演算，该演算终止、消去切割，并为 KM 提供了可判定性论证。然后，我们将 Pitts 的技术调整到我们的演算中，以构造 KM 的均匀插值，同时强调我们克服的障碍。最后，通过（重新）证明 KM 的可代数化性，我们推导出 KM-代数类的连贯性。我们所有的结果都在 Rocq 证明助手中完全机械化，确保了正确性并实现了插值的有效计算。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
