ウィキペディア |
 
|
エルブランの定理
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2012/02/10 08:56 UTC 版)
エルブランの定理（英: Herbrand's theorem）は1930年にジャック・エルブランが発表した数理論理学上の基本定理である [1]。 エルブランの定理は様々な表現方法があるが、単純には以下のように表現できる。
- F を節の有限集合とするとき、以下の2つは同値である。
- F が充足不能
- F から得られる基礎例（エルブラン基底）の有限集合で充足不能なものが存在
エルブランの定理は一階述語論理における任意の恒真な論理式の証明が有限回の機械的な操作で終わることを保証し、ほとんどの自動定理証明の理論的な基盤になっている。チューリングマシンの停止性問題と同様、一般的な述語論理式が証明可能かどうかを求めるアルゴリズムは存在しないが、エルブランの定理では一階述語論理を命題論理と結び付けることで、一階述語論理での証明可能性についての部分的な回答を与えている。
なお、エルブランの本来の証明は任意の一階述語論理式を対象としたものだが[2]、多くの場合、冠頭形の論理式に制限し単純化した定理で表される。
|
|||||||||||||
- ^ J. Herbrand, Recherches sur la théorie de la démonstration. Travaux de la Societe des Sciences et des Lettres de Varsovie, Class III, Sciences Mathematiques et Physiques, 33, pp.33-160, 1930.
- ^ a b Buss, Samuel R., "On Herbrand's Theorem", in Maurice, Daniel; Leivant, Raphaël, Logic and Computational Complexity, Lecture Notes in Computer Science, Springer-Verlag, pp. 195–209. 1995.
[続きの解説]
「エルブランの定理」の続きの解説一覧
- 1 エルブランの定理とは
- 2 エルブランの定理の概要
- 3 関連項目
固有名詞の分類
エルブランの定理に関係した商品
- 【送料無料】情報科学における論理楽天ブックス
- 【送料無料】岩波講座ソフトウェア科学（11）楽天ブックス
エルブランの定理のページへのリンク
