クレイグの補間定理（英: Craig's interpolation theorem）は論理学における定理であり、論理体系によってその定義が異なる。William Craig が1957年、一階述語論理について証明したのが最初である。クレイグの補題とも。命題論理版は以下のように定義される。が恒真式であるとき、論理式 formula_2 の全ての命題変数が formula_3 と formula_4 の両方に出現する場合で、かつとも恒真式なら、formula_2 をの「補間（interpolant）」と呼ぶ。単純な例として、次の式に対して formula_9 は補間である。命題論理でのクレイグの補間定理は、含意が恒真式なら、常に補間が存在する、というものである。クレイグの補間定理は以下のような方法で証明できる。クレイグの補間定理は、一貫性の証明、モデル検査、モジュール仕様の証明、モジュールオントロジーの証明などに使われる。

出典:wikipedia