On the Completeness of Interpolation Algorithms

Craig interpolation is a fundamental property of classical and non-classic 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 $\mathcal{I}$ is \emph{complete} if, for every semantically possible interpolant $C$ of an implication $A \to B$, there is a proof $P$ of $A \to B$ such that $C$ is logically equivalent to $\mathcal{I}(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.