翻訳と辞書 Words near each other ・ 節後迷走神経刺激 ・ 節抜き ・ 節操 ・ 節政貴弘 ・ 節日 ・ 節月 ・ 節板 ・ 節果 ・ 節榑 ・ 節榑立つ ・ 節標準形 ・ 節欲 ・ 節止め ・ 節気 ・ 節水 ・ 節水コマ ・ 節水栽培 ・ 節炭器 ・ 節点 ・ 節煙 Dictionary Lists mini英和辞書 mini和英辞書 Webster 1913 Latin-English FOLDOC Wikipedia English ウィキペディア

翻訳と辞書　辞書検索 [ 開発暫定版 ] スポンサード リンク 節標準形 ： ウィキペディア日本語版 節標準形[ふしひょうじゅんがた] 節標準形（英: Clausal normal form、CNF）とは、数理論理学において、論理プログラミングや多くの自動定理証明系で使われる論理式の標準形式である。論理式を節標準形に変換すると論理式の構造が破壊される。また、Tseitin transformation を使用せずに単純な変換をすると式のサイズが最悪ケースではする。 == 変換手順 == 古典的な一階述語論理の論理式を節標準形に変換する手順は以下の通りである。 # 論理式を否定標準形にする。 # スコーレム化 -- 外から内に向かって、存在量化変項をスコーレム定数に置き換え、全称量化変項をスコーレム関数に置き換えていく。具体的には次のような置換を行う。 # * $\backslash forall\; x\; \backslash ,\; P(x)$ を $\backslash exists\; c\; \backslash ,\; P(c)$ とする。ここで $c$ は新規導入。 # * $\backslash forall\; x\; \backslash exists\; y\; \backslash ,\; P(y)$ を $,\; \backslash forall\; x\; \backslash ,\; P(f\_c(x))$ とする。ここで $f\_c$ は新規導入。 # 全称量化子を削除する。 # 論理式を連言標準形にする。 # $C1\; \backslash wedge\; ...\; \backslash wedge\; Cn$ を $\backslash$ に置換。それぞれの論理積は $\backslash neg\; A1\; \backslash vee\; ...\; \backslash vee\; \backslash neg\; Am\; \backslash vee\; B1\; \backslash vee\; ...\; \backslash vee\; Bn$ という形式になり、これは $(\; A1\; \backslash wedge\; ...\; \backslash wedge\; Am\; )\; \backslash to\; (\; B1\; \backslash vee\; ...\; \backslash vee\; Bn\; )$ と等価である。 # * m=0 かつ n=1 なら、Prolog における事実となる。 # * m>0 かつ n=1 なら、Prolog における規則となる。 # * m>0 かつ n=0 なら、Prolog におけるクエリとなる。 # 最後に各論理積 $(\; A1\; \backslash wedge\; ...\; \backslash wedge\; Am\; )\; \backslash to\; (\; B1\; \backslash vee\; ...\; \backslash vee\; Bn\; )$ を $\backslash$ に置換する。 n = 1 の場合をホーン節と呼び、これは万能チューリング機械と同等の計算能力を有する。 完全な等価でなくとも、同等（equisatisfiable）な節標準形で十分であることが多い。その場合、指数関数的増大を防ぐには、Tseitin transformation を使用し、定義（definitions）を導入して論理式の一部を改名（rename）すればよい。 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「節標準形」の詳細全文を読む スポンサード リンク 翻訳と辞書 : 翻訳のためのインターネットリソース Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.