CNF 乗法標準形 Conjunctive normal form メモ

ここ数日前から「メモ」とタイプしようとすると、なぜか「モエ」と打ち間違えてしまう。

modus ponens
肯定式

リテラル
論理変数x　 またはその否定 ¬x　のこと
素式あるいは否定の付いた素式のこと。

節(clause)　リテラルを∨で繋げたもの。

すべての述語論理式は3-CNF（節の中にリテラルが3つのかたち）に変換が可能。

3-CNFの例
(x1∨x2∨x3)∧(x4∨x5∨x6)∧(x7∨x8∨x9)
のような形になっている。

CNFのルール
節の中のリテラルを繋ぐのは　∨　のみ
節同士を繋ぐのは　∧　のみ　
¬　は　リテラルの中だけにつけること

■CNFに変換する例　

お題　：　A⇔（B∨C）

まず、a⇔b　は　(a⇒b)∧(b⇒a)　に変換可能なので、

（A⇒（B∨C）)∧(（B∨C）⇒A)

次に、a⇒bは　¬a∨b　に変換可能なので、

（¬A∨（B∨C）)∧(¬（B∨C）∨A)

次に、　¬をリテラルに付ける。　（１）¬(a∨b)≡¬a∧¬b　（２）¬(a∧b)≡¬a∨¬b　　（ド・モルガンの法則）より、

（１）を使って、
（¬A∨（B∨C）)∧((¬B∧¬C）∨A)

次に、　節を∧で繋げた形にする。　（３）a∨(b∧c)≡(a∨b)∧(a∨c)　（４）a∧(b∨c)≡(a∧b)∨(a∧c)

（３）を使って、
（¬A∨B∨C)∧(¬B∨A)∧(¬C∨A)　これは　CNF