Interpolation in first-order logic with equality

Abstract

Craig's interpolation theorem is a long known basic result of mathematical logic. Interpolants lay bare certain logical relations between formulas or sets of formulas in a concise way and can often be calculated efficiently from proofs of these relations. Leveraging the tremendous progress of automatic deduction systems in the last decades, obtaining the required proofs is feasible. This enables real world applications for instance in the area of software verification. For practical applicability, interpolation is often studied in relatively weak formalisms such as propositional logic. This thesis however aims at giving a comprehensive account of existing techniques and results with respect to unrestricted classical first-order logic with equality. It is structured into three parts: First, we present Craig's initial proof of the interpolation theorem by reduction to first-order logic without equality and function symbols. Due to the inherent overhead, this approach only gives rise to an impractical algorithm for interpolant extraction. Second, a constructive proof by Huang is introduced in slightly improved form. It employs direct interpolant extraction from resolution proofs in two phases and thereby shows that even in full first-order logic with equality, interpolants can efficiently be calculated. Moreover, we present an analysis of the number of quantifier alternations of the interpolants produced by this algorithm. We additionally propose a novel approach which combines the two phases of Huang's algorithm and thereby allows for creating non-prenex interpolants. Third, we give a semantic perspective on interpolation in the form of a model-theoretic proof based on Robinson's joint consistency theorem. This illustrates the similarities and differences between the proof-theoretic and the model-theoretic view on interpolation.