エルブランの定理

エルブランの定理（Herbrand's theorem）は1930年にジャック・エルブランが発表した数理論理学上の基本定理である。エルブランの定理は様々な表現方法があるが、単純には以下のように表現できる。:<math>F</math> を節の有限集合とするとき、以下の2つは同値である。:* <math>F</math> が充足不能:* <math>F</math> から得られる基礎例（エルブラン基底）の有限集合で充足不能なものが存在エルブランの定理は一階述語論理における任意の恒真な論理式の証明が有限回の機械的な操作で終わることを保証し、ほとんどの自動定理証明の理論的な基盤になっている。チューリングマシンの停止性問題と同様、一般的な述語論理式が証明可能かどうかを求めるアルゴリズムは存在しないが、エルブランの定理では一階述語論理を命題論理と結び付けることで、一階述語論理での証明可能性についての部分的な回答を与えている。なお、エルブランの本来の証明は任意の一階述語論理式を対象としたものだが、多くの場合、冠頭形の論理式に制限し単純化した定理で表される。