This chapter provides a comprehensive overview of proof-theoretic methods for establishing interpolation properties across a range of logics, including classical, intuitionistic, modal, and substructural logics. Central to the discussion are two foundational techniques: Maehara's method for Craig interpolation and Pitts' method for uniform interpolation. The chapter demonstrates how these methods lead to results on the existence of well-behaved proof systems in the contemporary framework of universal proof theory and how they provide a road map for constructing interpolation proofs using modern proof formalisms. The emphasis of the chapter is on constructive, modular, and syntax-driven techniques that illuminate deeper connections between interpolation properties and proof systems.

翻译：本章全面综述了证明论方法在确立各类逻辑（包括经典逻辑、直觉主义逻辑、模态逻辑与子结构逻辑）插值性质中的应用。讨论的核心是两种基础性技术：针对Craig插值的Maehara方法以及针对一致插值的Pitts方法。本章展示了这些方法如何在当代通用证明论框架下导出具有良好性质的证明系统的存在性结果，并阐明了如何利用现代证明形式体系构建插值证明的路线图。本章重点在于构造性、模块化及语法驱动的技术，这些技术揭示了插值性质与证明系统之间更深层次的联系。