Craig Interpolation

Natural & Formal Sciences Dictionary
A metatheorem and constructive procedure which, given a proof that formula A implies formula B in a logic, produces an intermediate formula I (an interpolant) that uses only the nonlogical symbols common to A and B and satisfies A entails I and I entails B.