翻訳と辞書 Words near each other ・ エルフ大人の缶詰 ・ エルフ版 下級生 あなただけを見つめて… ・ エルフ版 下級生～あなただけを見つめて～ ・ エルフ語 ・ エルブジ ・ エルブスコ ・ エルブス反応 ・ エルブス過硫酸酸化 ・ エルブス酸化 ・ エルブラス・テデエフ ・ エルブランの定理 ・ エルブリ ・ エルブリッジ・ゲリー ・ エルブルス ・ エルブルス山 ・ エルブルズ山 ・ エルブルズ山脈 ・ エルブルワリー ・ エルブルース ・ エルブルース山 Dictionary Lists mini英和辞書 mini和英辞書 Webster 1913 Latin-English FOLDOC Wikipedia English ウィキペディア

翻訳と辞書　辞書検索 [ 開発暫定版 ] スポンサード リンク エルブランの定理 ： ウィキペディア日本語版 エルブランの定理[えるぶらんのていり] エルブランの定理（）は1930年にジャック・エルブランが発表した数理論理学上の基本定理である 〔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.〕。 エルブランの定理は様々な表現方法があるが、単純には以下のように表現できる。 :$F$ を節の有限集合とするとき、以下の2つは同値である。 : * $F$ が充足不能 : * $F$ から得られる基礎例（エルブラン基底）の有限集合で充足不能なものが存在 エルブランの定理は一階述語論理における任意の恒真な論理式の証明が有限回の機械的な操作で終わることを保証し、ほとんどの自動定理証明の理論的な基盤になっている。チューリングマシンの停止性問題と同様、一般的な述語論理式が証明可能かどうかを求めるアルゴリズムは存在しないが、エルブランの定理では一階述語論理を命題論理と結び付けることで、一階述語論理での証明可能性についての部分的な回答を与えている。 なお、エルブランの本来の証明は任意の一階述語論理式を対象としたものだが〔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.〕、多くの場合、冠頭形の論理式に制限し単純化した定理で表される。 == エルブラン領域 == エルブラン領域（）とは、述語論理式に現れうる変数を含まない全ての項の集合である。 述語論理式の''項''は以下の定義から帰納的に表される。 * 任意の個体定項（''定数''）は項である。 * 任意の個体変項（''変数''）は項である。 * 任意の n 引数の''関数記号'' ''f'' と複数の項からなる ''f(t1, .. ,tn)'' は項である。 論理式を構成する記号として定数及び関数記号が定められているとき、変数を含まない項（''閉項''、'）の全体を''エルブラン領域''（'）といい、以下の式 ''H'' で表すことができる。論理式に定数が含まれない場合は任意の定数 c を付加する。 :$H\; =\backslash textstyle\; H\_$ : * $H\_0\; =\; \backslash big\backslash$ （cは定数記号） : * $H\_\; =\; H\_i\; \backslash cup\; \backslash big\backslash$ （''f'' は n 引数の関数記号） 例えば、定数 ''a'' と1引数関数 ''f'' 及び2引数関数 ''g'' が論理式に含まれる場合のエルブラン領域は、''a, f(a), f(f(a)), g(a,a), g(a,f(a)), f(g(a,a)), g(a,g(a,a)), ‥ '' となる。）の全体を''エルブラン領域''（'）といい、以下の式 ''H'' で表すことができる。論理式に定数が含まれない場合は任意の定数 c を付加する。 :$H\; =\backslash textstyle\; H\_$ : * $H\_0\; =\; \backslash big\backslash$ （cは定数記号） : * $H\_\; =\; H\_i\; \backslash cup\; \backslash big\backslash$ （''f'' は n 引数の関数記号） 例えば、定数 ''a'' と1引数関数 ''f'' 及び2引数関数 ''g'' が論理式に含まれる場合のエルブラン領域は、''a, f(a), f(f(a)), g(a,a), g(a,f(a)), f(g(a,a)), g(a,g(a,a)), ‥ '' となる。）といい、以下の式 ''H'' で表すことができる。論理式に定数が含まれない場合は任意の定数 c を付加する。 :$H\; =\backslash textstyle\; H\_$ : * $H\_0\; =\; \backslash big\backslash$ （cは定数記号） : * $H\_\; =\; H\_i\; \backslash cup\; \backslash big\backslash$ （''f'' は n 引数の関数記号） 例えば、定数 ''a'' と1引数関数 ''f'' 及び2引数関数 ''g'' が論理式に含まれる場合のエルブラン領域は、''a, f(a), f(f(a)), g(a,a), g(a,f(a)), f(g(a,a)), g(a,g(a,a)), ‥ '' となる。 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「エルブランの定理」の詳細全文を読む スポンサード リンク 翻訳と辞書 : 翻訳のためのインターネットリソース Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.