ギルモアのアルゴリズムのソースを表示

'''ギルモアのアルゴリズム'''（{{lang-en-short|''Gilmore's algorithm''}}）は、[[エルブランの定理]]にもとづき[[一階述語論理]]式が充足不能（''{{lang|en|unsatisfiable}}''）かどうかを調べる半アルゴリズム（''{{lang|en|semi-algorithm}}''）である。ギルモアのアルゴリズムは1960年に発表された。
<ref name=Gilmore1960>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.</ref>

== 概要 ==
一階述語論理式 ''P'' が証明可能かどうかを調べたい時、[[エルブランの定理]]により、
* ''P'' が[[恒真式|恒真]]かどうかは、<math>\lnot P</math> が充足不能（恒偽）かどうかと同値
* <math>\lnot P</math> が充足不能ならば、基礎例（''{{lang|en|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分以内で行った<ref name= Gilmore1960></ref>。
だが、基礎例を機械的に作り出しその充足不能性を調べるやり方は、多数の無駄な論理式が生成されるため効率が非常に悪く、単純な証明のみが可能だった<ref name=Davis2001>Davis Martin. ''The Early History of Automated Deduction''. in ''Handbook of Automated Reasoning'', ''Volume I'', Alan Robinson and Andrei Voronkov(ed), 2001. ISBN 9780444829498.</ref>。

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

== 関連項目 ==
* [[エルブランの定理]]
* [[定理自動証明]]
* [[導出|導出原理]]

== 参考文献 ==
*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.
* {{cite book
 | last = Gallier
 | first = Jean H.
 | title = Logic for Computer Science: Foundations of Automatic Theorem Proving
 | publisher = Harper & Row Publishers
 | year = 1986
 | url = http://www.cis.upenn.edu/~jean/gbooks/logic.html
}}

== 脚注 ==
<div class="references-small">
<references/>
</div>

{{DEFAULTSORT:きるもあのあるこりすむ}}
[[Category:アルゴリズム]]
[[Category:数理論理学]]
[[Category:形式手法]]
[[Category:数学に関する記事]]
[[Category:数学のエポニム]]