Interpolation de Craig (Théorème D'Interpolation de Craig)

Un méta-théorème et une procédure constructive qui, à partir d'une preuve que la formule A implique la formule B dans une logique, produit une formule intermédiaire I (un interpolant) qui n'utilise que les symboles non logiques communs à A et B et vérifie A implique I et I implique B.