We will discuss this paper by Hetzl and Jalali
Abstract:
Craig interpolation is a fundamental property of logics with a plethora of applications from philosophical logic to computer-aided verification. The question of which interpolants can be obtained from an interpolation algorithm is of profound importance. Motivated by this question, we initiate the study of completeness properties of interpolation algorithms. An interpolation algorithm ℐ is complete if, for every interpolant C of an implication A → B, there is a proof P of A → B such that C is logically equivalent to ℐ(P). We establish incompleteness and different kinds of completeness results for several standard algorithms for resolution and the sequent calculus for propositional, modal, and first-order logic.