翻訳と辞書 Words near each other ・ ギルベルト・フックス ・ ギルベルト・ラミレス ・ ギルボア山 ・ ギルボー・コラ ・ ギルマン試薬 ・ ギルマ・ウォルドギオルギス ・ ギルマー郡 (ウェストバージニア州) ・ ギルマー郡 (ジョージア州) ・ ギルメイ・ゲブレスラシエ ・ ギルモア ・ ギルモアのアルゴリズム ・ ギルモア・D・クラーク ・ ギルモア・ガールズ ・ ギルモア・クラーク ・ ギルモレオサウルス ・ ギルモン ・ ギルランディーナ ・ ギルロイ ・ ギルロイ (カリフォルニア州) ・ ギルワの戦い Dictionary Lists mini英和辞書 mini和英辞書 Webster 1913 Latin-English FOLDOC Wikipedia English ウィキペディア

翻訳と辞書　辞書検索 [ 開発暫定版 ] スポンサード リンク ギルモアのアルゴリズム ： ミニ英和和英辞書 ギルモアのアルゴリズム ===================================== 〔語彙分解〕的な部分一致の検索結果は以下の通りです。 ギルモアのアルゴリズム ： ウィキペディア日本語版 ギルモアのアルゴリズム ギルモアのアルゴリズム（）は、エルブランの定理にもとづき一階述語論理式が充足不能（'）かどうかを調べる半アルゴリズム（'）である。ギルモアのアルゴリズムは1960年に発表された。 〔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.〕）かどうかを調べる半アルゴリズム（'）である。ギルモアのアルゴリズムは1960年に発表された。 〔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.〕）である。ギルモアのアルゴリズムは1960年に発表された。 〔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.〕 == 概要 == 一階述語論理式 ''P'' が証明可能かどうかを調べたい時、エルブランの定理により、 * ''P'' が恒真かどうかは、$\backslash lnot\; P$ が充足不能（恒偽）かどうかと同値 * $\backslash lnot\; P$ が充足不能ならば、基礎例（'）の命題論理レベルの充足不能チェックにより有限ステップで証明可 であり、ギルモアのアルゴリズムはこの考え方をもとにしている。 アルゴリズムの入出力は以下のように定義できる。 : ここで $E\backslash left(F\backslash right)=\backslash left\backslash$ はエルブラン領域の要素を述語論理式に代入した基礎例（エルブラン基底）の集合で、アルゴリズムの入力である。 対象となる述語論理式は冠頭標準形にした選言標準形の式で表現される。 実際の手続きは以下のようになる: : * $k\; 1$ : * $\backslash wedge\_^k\; A\_i$ が充足不能（命題論理）でないなら、$kk+1$ とし繰り返す : * 停止する (結果:''F は充足不能'') この手続きは半決定可能で、証明したい論理式が充足不能でない場合、手続きは停止しない。一般に、述語論理式が証明可能かどうかは決定可能でないことが知られている。）の命題論理レベルの充足不能チェックにより有限ステップで証明可 であり、ギルモアのアルゴリズムはこの考え方をもとにしている。 アルゴリズムの入出力は以下のように定義できる。 : ここで $E\backslash left(F\backslash right)=\backslash left\backslash$ はエルブラン領域の要素を述語論理式に代入した基礎例（エルブラン基底）の集合で、アルゴリズムの入力である。 対象となる述語論理式は冠頭標準形にした選言標準形の式で表現される。 実際の手続きは以下のようになる: : * $k\; 1$ : * $\backslash wedge\_^k\; A\_i$ が充足不能（命題論理）でないなら、$kk+1$ とし繰り返す : * 停止する (結果:''F は充足不能'') この手続きは半決定可能で、証明したい論理式が充足不能でない場合、手続きは停止しない。一般に、述語論理式が証明可能かどうかは決定可能でないことが知られている。 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「ギルモアのアルゴリズム」の詳細全文を読む スポンサード リンク 翻訳と辞書 : 翻訳のためのインターネットリソース Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.