否定標準形
否定標準形(ひていひょうじゅんけい、英: negation normal form, NNF)とは、否定記号 ¬ {\displaystyle \lnot } が原子論理式のみにかかり、他には選言記号 ∨ {\displaystyle \lor } と連言記号 ∧ {\displaystyle \land } のみが論理記号として用いられる形の論理式を指す。
命題論理もしくは述語論理においては、いかなる論理式も、ド・モルガンの法則を用い否定演算子を内側に押し込む操作を繰り返すことによって、論理的に等価な否定標準形に置き換えることができる。この操作の具体例を次に示す。
¬ ( ∀ x . G ) → ∃ x . ¬ G {\displaystyle \lnot (\forall x.G)\to \exists x.\lnot G}
¬ ( ∃ x . G ) → ∀ x . ¬ G {\displaystyle \lnot (\exists x.