否定標準形

否定標準形（ひていひょうじゅんけい、英: negation normal form, NNF）とは、否定記号 [math]\lnot[/math] が原子論理式のみにかかり、他には選言記号 [math]\lor[/math] と連言記号 [math]\land[/math] のみが論理記号として用いられる形の論理式を指す。

命題論理もしくは述語論理においては、いかなる論理式も、ド・モルガンの法則を用い否定演算子を内側に押し込む操作を繰り返すことによって、論理的に等価な否定標準形に置き換えることができる。この操作の具体例を次に示す。

[math]\lnot (\forall x. G) \to \exists x. \lnot G[/math]

[math]\lnot (\exists x. G) \to \forall x. \lnot G[/math]

[math]\lnot \lnot G \to G[/math]

[math]\lnot (G_1 \land G_2) \to (\lnot G_1) \lor (\lnot G_2)[/math]

[math]\lnot (G_1 \lor G_2) \to (\lnot G_1) \land (\lnot G_2)[/math]

連言標準形(conjunctive normal form)と選言標準形(disjunctive normal form)は否定標準形の性質を満たしている。任意の否定標準形の論理式は、論理式の結合法則と分配法則による操作によって、論理的に等価な連言標準形や選言標準形に変形することができる。

関連項目

• 連言標準形
• 選言標準形