エルブランの定理(''Herbrand's theorem'')は1930年にジャック・エルブランが発表した数理論理学上の基本定理である。エルブランの定理は様々な表現方法があるが、単純には以下のように表現できる。:<math>F</math> を節の有限集合とするとき、以下の2つは同値である。:* <math>F</math> が充足不能:* <math>F</math> から得られる基礎例(エルブラン基底)の有限集合で充足不能なものが存在エルブランの定理は一階述語論理における任意の恒真な論理式の証明が有限回の機械的な操作で終わることを保証し、ほとんどの自......
エルブランの定理(''Herbrand's theorem'')は1930年にジャック・エルブランが発表した数理論理学上の基本定理である。エルブランの定理は様々な表現方法があるが、単純には以下のように表現できる。:<math>F</math> を節の有限集合とするとき、以下の2つは同値である。:* <math>F</math> が充足不能:* <math>F</math> から得......