We consider interpolation from the viewpoint of fully automated theorem proving in first-order logic as a general core technique for mechanized knowledge processing. For Craig interpolation, our focus is on the two-stage approach, where first an essentially propositional ground interpolant is calculated that is then lifted to a quantified first-order formula. We discuss two possibilities to obtain a ground interpolant from a proof: with clausal tableaux, and with resolution. Established preprocessing techniques for first-order proving can also be applied for Craig interpolation if they are restricted in specific ways. Equality encodings from automated reasoning justify strengthened variations of Craig interpolation. Contributions to Craig interpolation that emerged from automated reasoning include variations for logics used in databases and logic programming. As an approach to uniform interpolation we introduce second-order quantifier elimination with examples and describe the basic algorithms DLS and SCAN.

翻译：本文从一阶逻辑全自动定理证明的视角探讨插值问题，将其视为机械化知识处理的通用核心技术。针对Craig插值，我们重点研究两阶段方法：首先计算本质上是命题逻辑的基插值式，随后将其提升为量化的一阶公式。我们讨论从证明中获取基插值式的两种途径：基于子句表推演系统与基于归结原理。一阶证明中成熟的预处理技术经过特定限制后同样适用于Craig插值。源自自动推理的等式编码技术为Craig插值提供了强化变体。自动推理领域对Craig插值的贡献包括面向数据库与逻辑编程所用逻辑的插值变体。作为均匀插值的一种实现路径，我们通过算例引入二阶量词消去方法，并阐述DLS与SCAN两种基础算法。