エルブランの定理
これはエルブランの定理の重要な成果である。
それとは反対に、F が充足可能のとき、全ての n に対し Q ( a 1 , . . . , a n ) {\displaystyle Q(a_{1},...,a_{n})} が真となり、変数 a i {\displaystyle a_{i}} が有限でない場合は計算が終わらない。これは、一般に述語計算が決定可能でないことを示している。
より形式的には、エルブランの定理は上の(2)、(3)について、論理式 S ( x , y ) {\displaystyle S(x,y)} をより一般化した形で表現される。また対象となる論理式は冠頭標準形の式である。以下に形式化されたエルブランの定理の例を示す。
( ∃ y 1 , ... , y n ) F ( y 1 , ... , y n ) {\displaystyle (\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})} を一階述語論理式とする。ここで F ( y 1 , ... , y n ) {\displaystyle F(y_{1},\ldots ,y_{n})} は量化子を1つも含まない論理式である。
このとき ( ∃ y 1 , ... , y n ) F ( y 1 , ...
エルブランの定理は自動定理証明の理論的基盤となった。
さらにエルブランの定理を計算機上で直接応用する試みが行われ、ギルモアのアルゴリズム(1960)やデービス・パトナムのアルゴリズム(1958,1960)が考案された。 これらはエルブランの定理の証明を直接計算機上で実行するようなやり方だったため、多数の不要な基礎例の生成が行われ、効率的ではなかった。
1965年にJ. Robinsonは単一化に基づく導出原理を発表した。導出原理ではただ1つの推論規則 A ∨ B , ¬ A ∨ C B ∨ C {\displaystyle {\frac {A\vee B,\lnot A\vee C}{B\vee C}}} を用い、エルブランの定理により証明したい論理式の否定から空節が導かれること(反駁)により証明を行う。
推論の過程で多数の基礎例の生成を行うのではなく単一化により必要な基礎例のみを段階的に具体化していくことで、導出原理では効率的な推論が可能になり、その後の定理証明やPrologなどの論理プログラミング言語に大きな影響を与えた。
エルブランの定理(英: Herbrand's theorem)は1930年にジャック・エルブランが発表した数理論理学上の基本定理である 。 エルブランの定理は様々な表現方法があるが、単純には以下のように表現できる。
F {\displaystyle F} を節の有限集合とするとき、以下の2つは同値である。 F {\displaystyle F} が充足不能 F {\displaystyle F} から得られる基礎例(エルブラン基底)の有限集合で充足不能なものが存在
エルブランの定理は一階述語論理における任意の恒真な論理式の証明が有限回の機械的な操作で終わることを保証し、ほとんどの自動定理証明の理論的な基盤になっている。チューリングマシンの停止性問題と同様、一般的な述語論理式が証明可能かどうかを求めるアルゴリズムは存在しないが、エルブランの定理では一階述語論理を命題論理と結び付けることで、一階述語論理での証明可能性についての部分的な回答を与えている。
なお、エルブランの本来の証明は任意の一階述語論理式を対象としたものだが、多くの場合、冠頭形の論理式に制限し単純化した定理で表される。