エルブランの定理（）は1930年にジャック・エルブランが発表した数理論理学上の基本定理であるエルブランの定理は様々な表現方法があるが、単純には以下のように表現できる。エルブランの定理は一階述語論理における任意の恒真な論理式の証明が有限回の機械的な操作で終わることを保証し、ほとんどの自動定理証明の理論的な基盤になっている。チューリングマシンの停止性問題と同様、一般的な述語論理式が証明可能かどうかを求めるアルゴリズムは存在しないが、エルブランの定理では一階述語論理を命題論理と結び付けることで、一階述語論理での証明可能性についての部分的な回答を与えている。なお、エルブランの本来の証明は任意の一階述語論理式を対象としたものだが、多くの場合、冠頭形の論理式に制限し単純化した定理で表される。エルブラン領域（）とは、述語論理式に現れうる変数を含まない全ての項の集合である。述語論理式の"項"は以下の定義から帰納的に表される。論理式を構成する記号として定数及び関数記号が定められているとき、変数を含まない項（"閉項"、'）の全体を"エルブラン領域"（'）といい、以下の式 "H" で表すことができる。論理式に定数が含まれない場合は任意の定数 c を付加する。例えば、定数 "a" と1引数関数 "f" 及び2引数関数 "g" が論理式に含まれる場合のエルブラン領域は、"a, f(a), f(f(a)), g(a,a), g(a,f(a)), f(g(a,a)), g(a,g(a,a)), ‥ " となる。エルブラン領域の全ての要素を論理式を構成する原子論理式に割り当て、それぞれの真偽値を決めることで、論理式に対する任意の解釈が表現できる。エルブラン領域の要素を引数とする原子論理式の全体をエルブラン基底（）という。例えば、"x, y, z"を変数とする述語 "P(x)" と "Q(g(a,y),f(z))" からなる論理式のエルブラン基底は、"P(a), P(f(a)), P(f(f(a))), P(g(a,a)), P(g(a,f(a))), ‥ ,Q(g(a,a),f(a)), ‥ " となる。一般に変数をもたない述語または節のことを"基礎例"(") と言う。エルブラン基底は節集合から得られる基礎例である。エルブラン基底を導入することで、論理式を命題論理式として扱うことができ、論理式の意味を構文的に決めることができる。エルブラン基底の任意の部分集合 "I" をエルブラン解釈（）と呼ぶ。直感的には、エルブラン基底の要素の内 "I" に含まれるものは真、それ以外は偽を表し、真偽値の割り当てにより論理式全体に対する1つの解釈を定めたことになる。エルブランの定理は、以下のように表現できる。つまり、一階述語論理式の充足不能性の判定は、エルブラン基底上の有限回の命題論理レベルでの判定で行うことができる。エルブランの定理はこれ以外にも様々な形式で表現することができる。一般に、論理式の真偽値は対象となる領域 "D" とその解釈 "I" の組（モデル）により異なる。例えば、formula_10 は、自然数を領域とするか実数を領域とするかで真偽値が変わる。モデルにより以下の3通りが考えられる。以下では、例として formula_11 のような全称論理式(あるいは論理式の集合) formula_1 を考える。formula_13 は述語、 formula_14 は変数の集まりを表す。以下の3つの特性について考える。ゲーデルの完全性定理は上の(1)と(2)が同値であると主張している。さらに(2)は(3)を含み、(3)で真となるモデルは(2)のモデルとなる。エルブランの定理は逆に、エルブラン領域という特定の領域で(3)が(2)を含んでいるということを主張する。つまり、エルブラン領域という特定の領域で考えると、上の(2)と(3)はエルブランの定理の別の表現であり、(1)、(2)、(3)は同値である。なお、エルブラン領域では変数が無くなるため(3)での全称記号が消え、解くべき論理式は命題論理の命題として扱うことができる。"G" = "¬F"、"R" = "¬Q"、"S" = "¬P" と置いて双対を考えると、上と等価な3つの特性を得ることができる。前と同様、上の(2)と(3)はエルブランの定理の別の表現であり、(1)、(2)、(3)は同値である。ここで、"F" が充足不能のとき（すなわち "G" = "¬F" が恒真のとき）を考える。formula_24 をformula_42、formula_43 と調べていくと、formula_24 が偽となるような "n" が存在する（そうでなければ全ての "n" で真となるため充足可能となってしまう）。またその逆も成り立つ。これを利用し、任意の恒真な論理式 "G" の証明を行いたい場合、論理式の否定 "¬G" の充足不能性を調べることで、エルブラン解釈の下での有限回の操作で調べることができる。これはエルブランの定理の重要な成果である。それとは反対に、"F" が充足可能のとき、全ての "n" に対し formula_24 が真となり、変数 formula_46 が有限でない場合は計算が終わらない。これは、一般に述語計算が決定可能でないことを示している。より形式的には、エルブランの定理は上の(2)、(3)について、論理式 formula_47 をより一般化した形で表現される。また対象となる論理式は冠頭標準形の式である。以下に形式化されたエルブランの定理の例を示す。formula_48 を一階述語論理式とする。ここで formula_49 は量化子を1つも含まない論理式である。このとき formula_48 が恒真になる必要十分条件は、ある自然数 formula_51 とエルブラン領域の項 formula_52 （formula_53）が存在し、が恒真になることである。このようなエルブランの定理の証明は、ゲーデルの完全性定理により恒真性が証明可能性に置き換えられることを利用し、ゲンツェンのカット除去定理を用い formula_55 のカット規則を除去した証明を求めるものが一般的である。エルブランが定理を証明した時にゲンツェンのカット除去定理はまだ知られておらず、ゲーデルの完全性定理も発表されていなかった。そのためエルブランによる証明はエルブラン版のカット除去定理や独自の完全性定理を含むもので、任意の一階述語論理式を対象としていた。エルブランの定理は自動定理証明の理論的基盤となった。さらにエルブランの定理を計算機上で直接応用する試みが行われ、ギルモアのアルゴリズム(1960)やデービス・パトナムのアルゴリズム(1958,1960)が考案された。これらはエルブランの定理の証明を直接計算機上で実行するようなやり方だったため、多数の不要な基礎例の生成が行われ、効率的ではなかった。1965年にJ. Robinsonは単一化に基づく導出原理を発表した。導出原理ではただ1つの推論規則 formula_56 を用い、エルブランの定理により証明したい論理式の否定から空節が導かれること（反駁）により証明を行う。推論の過程で多数の基礎例の生成を行うのではなく単一化により必要な基礎例のみを段階的に具体化していくことで、導出原理では効率的な推論が可能になり、その後の定理証明やPrologなどの論理プログラミング言語に大きな影響を与えた。

出典:wikipedia