ギルモアのアルゴリズム

ギルモアのアルゴリズムについて

ギルモアのアルゴリズムは、エルブランの定理を基にした一階述語論理式の充足不能性を調査するための半アルゴリズムです。このアルゴリズムは1960年に発表され、その後の論理学やコンピュータ科学において重要な役割を果たしました。

アルゴリズムの概要

一階述語論理式 P の証明可能性を検討する際、エルブランの定理により、P が恒真であるかどうかは、その否定 9;P が充足不能（すなわち、恒偽である）であるかどうかと同じ意味を持ちます。つまり、条件が満たされる場合、P が充足不能であれば、有限のステップで証明が可能であるということです。ギルモアのアルゴリズムはこの理論的な枠組みに基づいています。

アルゴリズムの入出力は次のように定義されます。エルブラン領域 E(F) は、述語論理式に対して定義される基礎例のセットであり、アルゴリズムの入力となります。対象となる論理式は、典型的には冠頭標準形（CNF）または選言標準形で表現されます。

アルゴリズムは以下の手順で進行します:
1. 変数 k を1に初期化します。
2. 述語論理式の基礎例が充足不能でない場合、k を1増加させ、手続きを繰り返します。
3. 充足不能性が導かれた時点で手続きは停止し、結果を出力します。

このプロセスは半決定可能であり、充足不能でない場合、手続きは無限に続いてしまう可能性があります。このため、一般的に述語論理式が証明可能かどうかは決定不可能であることが知られています。

アルゴリズムの実用性

ギルモアのアルゴリズムはIBM 704でプログラムされ、適度に複雑な論理式に対する証明を短時間で実行しました。しかし、基礎例を機械的に生成し、その充足可能性を調べる手法には多くの無駄が伴い、効率が悪く、単純な証明しかできませんでした。それにもかかわらず、このアルゴリズムは自動定理証明の初期の試みの一つであり、後の研究における刺激となりました。

例えば、導出原理や他の証明手法の発展に寄与しました。ギルモアのアルゴリズムを通じて、論理学の複雑さを扱うための新たなアプローチが確立され、今後の研究に影響を与えました。

関連項目

• - エルブランの定理：ギルモアのアルゴリズムの基礎となる理論。
• - 定理自動証明：論理式の証明を自動化する技術。
• - 導出原理：論理的な推論を行うための法則。

参考文献

• - 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(編著), 2001.
• - Wolfgang Bibel. Early History and Perspectives of Automated Deduction. in Advances in Artificial Intelligence, Lecture Notes in Computer Science, Springer-Verlag Berlin, 2007.

ギルモアのアルゴリズムは、論理に関する研究における重要な一歩を示しており、その後の発展における礎となりました。

もう一度検索