選言標準形

選言標準形（せんげんひょうじゅんけい、英: Disjunctive normal form, DNF）は、数理論理学においてブール論理での論理式の標準化（正規化）の一種であり、連言節(AND)の選言(OR)の形式で論理式を表す。加法標準形、主加法標準形、積和標準形とも呼ぶ。正規形としては、自動定理証明で利用されている。

概要

選言標準形の論理式は、1つ以上のリテラルの論理積を1つ以上含む論理和の形式になっている論理式を選言標準形と呼ぶ。連言標準形(CNF)と同様、DNF における演算子は論理積、論理和、否定だけである。

以下の論理式は DNF の一種である。

$A\lor B$

$A\!$

$(A\land B)\lor C$

$(A\land \neg B\land \neg C)\lor (\neg D\land E\land F)$

しかし、以下の論理式は DNF ではない。

$\neg (A\lor B)$ — NOT が最も外側の演算子になっている

$A\lor (B\land (C\lor D))$ — OR が AND の内側にある

リテラルは、変項（命題）か変項の否定であり、否定演算子はこの形でのみ出現する。全ての変項（またはその否定）を含む論理式を標準項と呼び、特に全ての変項（またはその否定）の論理積の形式になっている項を最小項と呼ぶ。従って、最小項の論理和の形式になっている論理式は、DNF である。この形式は、真理値表で出力が「真」となる行を最小項として取り出したものを論理和で繋いだものであり、その真理値表に対応する論理式となっている。つまり、真理値表で表されるものは全て選言標準形の論理式で表せ、組み合わせ回路も選言標準形で表せる。

任意の論理式を DNF に変換するには、二重否定の除去、ド・モルガンの法則、分配法則といった論理的に等価な変換を行う法則を使う。全ての論理式は選言標準形に変換できる。しかし、元の論理式によっては、DNF への変換によって論理式が極めて長大になることもある。例えば、次の論理式を DNF に変換すると、2ⁿ 個の項を書き連ねることになる。

$(X_{1}\lor Y_{1})\land (X_{2}\lor Y_{2})\land \dots \land (X_{n}\lor Y_{n})$

以下は、DNF の形式文法である:

1. <or> → ∨
2. <and> → ∧
3. <not> → ¬
4. <disjunct> → <conjunct>
5. <disjunct> → <disjunct> <or> <conjunct>
6. <conjunct> → <literal>
7. <conjunct> → (<conjunct> <and> <literal>)
8. <literal> → <term>
9. <literal> → <not><term>

ここで <term> は任意の変項である。

関連項目

• リード-マラー標準形
• ブール関数
• ブール値関数
• 連言標準形
• ホーン節
• クワイン・マクラスキー法
• 真理値表