ギルモアのアルゴリズム

ギルモアのアルゴリズム（英: Gilmore's algorithm）は、エルブランの定理にもとづき一階述語論理式が充足不能（unsatisfiable）かどうかを調べる半アルゴリズム（semi-algorithm）である。ギルモアのアルゴリズムは1960年に発表された。

概要

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

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

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

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

[math]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}[/math]

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

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

• [math]k {:=} 1[/math]
• [math]\wedge_{i=1}^k A_i[/math] が充足不能（命題論理）でないなら、[math]k{:=}k+1[/math] とし繰り返す
• 停止する (結果:F は充足不能)

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

展開

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

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

関連項目

• エルブランの定理
• 定理自動証明
• 導出原理

参考文献

• P. Gilmore. A proof method for quantification theory: its justification and realization. IBM Journal of Research and Development, Volume 4, Issue 1, pp.28-35. 1960.
• Davis Martin. The Early History of Automated Deduction. in Handbook of Automated Reasoning, Volume I, Alan Robinson and Andrei Voronkov(ed), 2001. ISBN 9780444829498.
• Wolfgang Bibel. Early History and Perspectives of Automated Deduction. in Advances in Artificial Intelligence, Lecture Notes in Computer Science, Springer-Verlag Berlin, 2007. ISBN 9783540745648.
• Gallier, Jean H. (1986). Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row Publishers.