ギルモアのアルゴリズム

一階述語論理式 P が証明可能かどうかを調べたい時、エルブランの定理により、

• P が恒真かどうかは、${\displaystyle \lnot P}$ が充足不能（恒偽）かどうかと同値
• ${\displaystyle \lnot P}$ が充足不能ならば、基礎例（ground instance）の命題論理レベルの充足不能チェックにより有限ステップで証明可

であり、ギルモアのアルゴリズムはこの考え方をもとにしている。

アルゴリズムの入出力は以下のように定義できる。

${\displaystyle Gilmore\left(E\left(F\right)\right)={\begin{cases}halt,&{\mbox{when }}F{\mbox{ is unsatisfiable}}\\undef,&{\mbox{when }}F{\mbox{ is not unsatisfiable}}\end{cases}}}$

ここで ${\displaystyle E\left(F\right)=\left\{A_{1},A_{2},...\right\}}$ はエルブラン領域の要素を述語論理式に代入した基礎例（エルブラン基底）の集合で、アルゴリズムの入力である。 対象となる述語論理式は冠頭標準形にした選言標準形の式で表現される。

実際の手続きは以下のようになる:

• ${\displaystyle k{:=}1}$
• ${\displaystyle \wedge _{i=1}^{k}A_{i}}$ が充足不能（命題論理）でないなら、${\displaystyle k{:=}k+1}$ とし繰り返す
• 停止する (結果:F は充足不能)

この手続きは半決定可能で、証明したい論理式が充足不能でない場合、手続きは停止しない。一般に、述語論理式が証明可能かどうかは決定可能でないことが知られている。

ギルモアのアルゴリズムはIBM 704上でプログラムされ、適度に複雑な論理式の証明を2分以内で行った^[1]。 だが、基礎例を機械的に作り出しその充足不能性を調べるやり方は、多数の無駄な論理式が生成されるため効率が非常に悪く、単純な証明のみが可能だった^[2]。

しかし、ギルモアのアルゴリズムは定理自動証明の初期の試みの1つとしてその後の研究の大きな刺激となり、導出原理などを生み出す原動力になった^[2]。