Craig-Interpolation (Craig'Scher Interpolationssatz)

Ein Metasatz und konstruktives Verfahren, das, gegeben einen Beweis dafür, dass Formel A Formel B impliziert, eine Zwischenformel I (Interpolant) liefert, die nur die nichtlogischen Symbole benutzt, die A und B gemeinsam haben, und so dass A I impliziert und I B impliziert.