Interpolación de Craig (Teorema de Interpolación de Craig)

Un metateorema y procedimiento constructivo que, dada una prueba de que la fórmula A implica la fórmula B en una lógica, produce una fórmula intermedia I (un interpolante) que utiliza sólo los símbolos no lógicos comunes a A y B y satisface que A implica I e I implica B.