We introduce Craig interpolation and related notions such as uniform interpolation, Beth definability, and theory decomposition in classical propositional logic. We present four approaches to computing interpolants: via quantifier elimination, from formulas in disjunctive normal form, and by extraction from resolution or tableau refutations. We close with a discussion of the size of interpolants and links to circuit complexity.

翻译：本文介绍了经典命题逻辑中的克雷格插值及相关概念，如均匀插值、贝特定理可定义性与理论分解。我们提出了四种计算插值式的方法：通过量词消去、从析取范式公式出发、以及从归结反驳或表反驳中提取。最后讨论了插值式的大小问题及其与电路复杂性的关联。