連言標準形

ブール論理では、式が1 つ以上の節の連言である場合、その式は連言正規形( CNF ) または節正規形です。ここで、節はリテラルの選言です。言い換えると、式は合計の積またはOR の ANDです。標準正規形として、自動定理証明や回路理論に役立ちます。

自動定理証明では、「節正規形」という概念は、リテラルのセットの集合としての CNF 式の特定の表現を意味する、より狭い意味で使用されることがよくあります。

論理式は、 1 つ以上のリテラルの1 つ以上の選言の連言である場合に CNF であると見なされます。選言標準形(DNF)と同様に、CNF の命題演算子はor ( )、and ( )、not ( ) のみです。not演算子はリテラルの一部としてのみ使用できます。つまり、命題変数の前にのみ置くことができます。 ${\displaystyle \vee}$${\displaystyle \wedge}$${\displaystyle \neg}$

以下はCNF の 文脈自由文法です。

1. CNF → (論理和) CNF${\displaystyle \land}$
2. CNF → (論理和)
3. 論理和→文字どおりの 論理和${\displaystyle \lor}$
4. 論理和→リテラル
5. リテラル→変数${\displaystyle \neg}$
6. リテラル→変数

ここで、Variable は任意の変数です。

変数、およびにおける次の式はすべて、連言正規形になっています。 ${\displaystyle A,B,C,D,E}$${\displaystyle F}$

• ${\displaystyle (A\lor \neg B\lor \neg C)\land (\neg D\lor E\lor F\lor D\lor F)}$
• ${\displaystyle (A\lor B)\land (C)}$
• ${\displaystyle (A\or B)}$
• ${\displaystyle (A)}$

次の式は連言正規形では ありません。

• ${\displaystyle \neg (A\land B)}$ANDがNOTの中にネストされているため
• ${\displaystyle \neg (A\lor B)\land C}$ORがNOTの中にネストされているため
• ${\displaystyle A\land (B\lor (D\land E))}$ANDはORの中にネストされているため

古典論理では、各命題式はCNFの同等の式に変換できます。 ^[1]この変換は、二重否定除去、ド・モルガンの法則、分配法則などの論理的同値性に関する規則に基づいています。

与えられた命題式のCNF相当値を計算するアルゴリズムは、選言標準形（DNF）のステップ1に基づいています。 ^[2] 次に、ANDとORを入れ替え、その逆を行いながら、すべてのリテラルを否定して、をに変換します。すべてのを削除します。^[1]${\displaystyle \phi}$${\displaystyle \lnot \phi }$
${\displaystyle \lnot \phi _{DNF}}$${\displaystyle \phi _{CNF}}$${\displaystyle \lnot \lnot }$

命題式を CNF に変換します。 ${\displaystyle \phi}$

ステップ1：その否定を選言標準形に変換する。^[2]

${\displaystyle \lnot \phi _{DNF}=(C_{1}\lor C_{2}\lor \ldots \lor C_{i}\lor \ldots \lor C_{m})}$、^​

ここで、それぞれはリテラルの連結である。^[b]${\displaystyle C_{i}}$${\displaystyle l_{i1}\land l_{i2}\land \ldots \land l_{in_{i}}}$

ステップ2 : を否定します。次に、（一般化された）ド・モルガンの同値を適用して、不可能になるまで内側に移動します。 ここで${\displaystyle \lnot \phi _{DNF}}$${\displaystyle \lnot}$$${\displaystyle {\begin{aligned}\phi &\leftrightarrow \lnot \lnot \phi _{DNF}\\&=\lnot (C_{1}\lor C_{2}\lor \ldots \lor C_{i}\lor \ldots \lor C_{m})\\&\leftrightarrow \lnot C_{1}\land \lnot C_{2}\land \ldots \land \lnot C_{i}\land \ldots \land \lnot C_{m}&&{\text{// (一般化) DM}}\end{aligned}}}$$$${\displaystyle {\begin{aligned}\lnot C_{i}&=\lnot (l_{i1}\land l_{i2}\land \ldots \land l_{in_{i}})\\&\leftrightarrow (\lnot l_{i1}\lor \lnot l_{i2}\lor \ldots \lor \lnot l_{in_{i}})&&{\text{// (一般化) DM}}\end{aligned}}}$$

ステップ 3 : すべての二重否定を削除します。

例

命題式をCNFに変換します 。^[c]${\displaystyle \phi =((\lnot (p\land q))\leftrightarrow (\lnot r\uparrow (p\oplus q)))}$

その否定に相当する（完全な）DNFは^{[2]である。}
${\displaystyle \lnot \phi _{DNF}=(p\land q\land r)\lor (p\land q\land \lnot r)\lor (p\land \lnot q\land \lnot r)\lor (\lnot p\land q\land \lnot r)}$

$${\displaystyle {\begin{aligned}\phi &\leftrightarrow \lnot \lnot \phi _{DNF}\\&=\lnot \{(p\land q\land r)\lor (p\land q\land \lnot r)\lor (p\land \lnot q\land \lnot r)\lor (\lnot p\land q\land \lnot r)\}\\&\leftrightarrow {\underline {\lnot (p\land q\land r)}}\land {\underline {\lnot (p\land q\land \lnot r)}}\land {\underline {\lnot (p\land \lnot q\land \lnot r)}}\land {\underline {\lnot (\lnot p\land q\land \lnot r)}}&&{\text{// generalized D.M. }}\\&\leftrightarrow (\lnot p\lor \lnot q\lor \lnot r)\land (\lnot p\lor \lnot q\lor \lnot \lnot r)\land (\lnot p\lor \lnot \lnot q\lor \lnot \lnot r)\land (\lnot \lnot p\lor \lnot q\lor \lnot \lnot r)&&{\text{// generalized D.M. }}(4\times )\\&\leftrightarrow (\lnot p\lor \lnot q\lor \lnot r)\land (\lnot p\lor \lnot q\lor r)\land (\lnot p\lor q\lor r)\land (p\lor \lnot q\lor r)&&{\text{// remove all }}\lnot \lnot \\&=\phi _{CNF}\end{aligned}}}$$

式のCNF相当は、その真理値表から導くことができます。もう一度、式を考えてみましょう 。^[c]$${\displaystyle \phi =((\lnot (p\land q))\leftrightarrow (\lnot r\uparrow (p\oplus q)))}$$

対応する真理値表は

CNFに相当するものは ${\displaystyle \phi }$$${\displaystyle (\lnot p\lor \lnot q\lor \lnot r)\land (\lnot p\lor \lnot q\lor r)\land (\lnot p\lor q\lor r)\land (p\lor \lnot q\lor r)}$$

各論理和は、F(alse)と評価される変数の割り当てを反映しています。 このような割り当てで変数${\displaystyle \phi }$
${\displaystyle V}$

• がT(真)の場合、リテラルは論理和で設定されます。${\displaystyle \lnot V}$
• が F(alse) の場合、リテラルは論理和で に設定されます。${\displaystyle V}$

すべての命題式は連言標準形の同等の式に変換できるため、証明は多くの場合、すべての式がCNFであるという仮定に基づいています。ただし、場合によっては、このCNFへの変換により、式の指数関数的爆発が発生する可能性があります。たとえば、非CNF式を変換すると、

$${\displaystyle (X_{1}\wedge Y_{1})\vee (X_{2}\wedge Y_{2})\vee \ldots \vee (X_{n}\wedge Y_{n})}$$

CNF にすると、次の節を含む式が生成されます。 ${\displaystyle 2^{n}}$

$${\displaystyle (X_{1}\vee X_{2}\vee \ldots \vee X_{n})\wedge (Y_{1}\vee X_{2}\vee \ldots \vee X_{n})\wedge (X_{1}\vee Y_{2}\vee \ldots \vee X_{n})\wedge (Y_{1}\vee Y_{2}\vee \ldots \vee X_{n})\wedge \ldots \wedge (Y_{1}\vee Y_{2}\vee \ldots \vee Y_{n}).}$$

各節には、それぞれまたはが含まれます。 ${\displaystyle X_{i}}$${\displaystyle Y_{i}}$${\displaystyle i}$

CNFへの変換には、同値性ではなく充足可能性を維持することで指数関数的なサイズの増加を回避するものがあります。^{[3] [4]}これらの変換では、式のサイズが線形に増加するだけで、新しい変数が導入されます。たとえば、上記の式は、次のように変数を追加することでCNFに変換できます。 ${\displaystyle Z_{1},\ldots ,Z_{n}}$

$${\displaystyle (Z_{1}\vee \ldots \vee Z_{n})\wedge (\neg Z_{1}\vee X_{1})\wedge (\neg Z_{1}\vee Y_{1})\wedge \ldots \wedge (\neg Z_{n}\vee X_{n})\wedge (\neg Z_{n}\vee Y_{n}).}$$

解釈がこの式を満たすのは、新しい変数の少なくとも 1 つが真である場合のみです。この変数が の場合、と も両方とも真です。つまり、この式を満たすすべてのモデルは、元の式も満たします。一方、元の式のモデルのうち、この式を満たすのは一部だけです。 は元の式で言及されていないため、その値は元の式を満たすこととは無関係ですが、最後の式ではそうではありません。つまり、元の式と翻訳の結果は等しく満たされますが、同等ではありません。 ${\displaystyle Z_{i}}$${\displaystyle X_{i}}$${\displaystyle Y_{i}}$${\displaystyle Z_{i}}$

代わりの翻訳であるTseitin 変換には、 という節も含まれます。これらの節により、式は を意味します。この式は、の名前として「定義」されているとよく考えられています。 ${\displaystyle Z_{i}\vee \neg X_{i}\vee \neg Y_{i}}$${\displaystyle Z_{i}\equiv X_{i}\wedge Y_{i}}$${\displaystyle Z_{i}}$${\displaystyle X_{i}\wedge Y_{i}}$

変数 を持つ命題式を考えます。 ${\displaystyle n}$${\displaystyle n\geq 1}$

可能なリテラルは次のとおりです: 。 ${\displaystyle 2n}$${\displaystyle L=\{p_{1},\lnot p_{1},p_{2},\lnot p_{2},\ldots ,p_{n},\lnot p_{n}\}}$

${\displaystyle L}$空でない部分集合を持つ。 ^[d]${\displaystyle (2^{2n}-1)}$

これはCNFが持つことができる論理和の最大数です。^[e]

すべての真理関数の組み合わせは、真理値表の各行に 1 つずつ、論理和で表現できます。以下の例では、論理和は下線で示されています。 ${\displaystyle 2^{n}}$

例

2 つの変数とを持つ式を考えます。 ${\displaystyle p}$${\displaystyle q}$

最も長いCNFには論理和がある: ^[e]${\displaystyle 2^{(2\times 2)}-1=15}$ $${\displaystyle {\begin{array}{lcl}(\lnot p)\land (p)\land (\lnot q)\land (q)\land \\(\lnot p\lor p)\land {\underline {(\lnot p\lor \lnot q)}}\land {\underline {(\lnot p\lor q)}}\land {\underline {(p\lor \lnot q)}}\land {\underline {(p\lor q)}}\land (\lnot q\lor q)\land \\(\lnot p\lor p\lor \lnot q)\land (\lnot p\lor p\lor q)\land (\lnot p\lor \lnot q\lor q)\land (p\lor \lnot q\lor q)\land \\(\lnot p\lor p\lor \lnot q\lor q)\end{array}}}$$

この式は矛盾している。

計算複雑性における重要な一連の問題には、論理積正規形で表現されたブール式の変数への割り当てを、式が真となるように見つけることが含まれます。k - SAT問題は、各選言に最大k 個の変数が含まれる CNF で表現されたブール式への満足な割り当てを見つける問題です。3 -SATはNP 完全( k >2の他のk -SAT 問題と同様に) ですが、 2-SAT は多項式時間で解けることが知られています。結果として、^[f]充足可能性を維持しながら式をDNFに変換するタスクはNP 困難です。双対的に、妥当性を維持しながら CNF に変換するタスクも NP 困難です。したがって、同値性を維持しながら DNF または CNF に変換することも NP 困難です。

この場合の典型的な問題には、「3CNF」の式が含まれます。これは、1 つの連言につき 3 つ以下の変数を持つ連言標準形です。実際に遭遇するこのような式の例は、たとえば 100,000 個の変数と 1,000,000 個の連言など、非常に大きくなる可能性があります。

CNF の式は、k個を超える変数を持つ各連言を 2 つの連言と新しい変数Zに置き換え、必要な回数だけ繰り返すことで、 「 k CNF」( k ≥ 3) の等充足式に変換できます。${\displaystyle X_{1}\vee \ldots \vee X_{k}\vee \ldots \vee X_{n}}$${\displaystyle X_{1}\vee \ldots \vee X_{k-1}\vee Z}$${\displaystyle \neg Z\vee X_{k}\lor \ldots \vee X_{n}}$

一階述語論理では、連言正規形をさらに進めることで論理式の節正規形が得られ、それを使って一階述語解決を実行することができる。解決ベースの自動定理証明では、CNF式

例については以下を参照してください。

一階論理をCNFに変換するには: ^[5]

1. 否定正規形に変換します。
   1. 含意と同値性を排除します。繰り返しを に置き換え、を に置き換えます。これにより、最終的にとのすべての出現が排除されます。${\displaystyle P\rightarrow Q}$${\displaystyle \lnot P\lor Q}$${\displaystyle P\leftrightarrow Q}$${\displaystyle (P\lor \lnot Q)\land (\lnot P\lor Q)}$${\displaystyle \rightarrow }$${\displaystyle \leftrightarrow }$
   2. ド・モルガンの法則を繰り返し適用して、NOT を内側に移動します。具体的には、を に置き換え、を に置き換え、を に置き換え、をに置き換えます。その後、 は述語記号の直前にのみ出現できます。${\displaystyle \lnot (P\lor Q)}$${\displaystyle (\lnot P)\land (\lnot Q)}$${\displaystyle \lnot (P\land Q)}$${\displaystyle (\lnot P)\lor (\lnot Q)}$${\displaystyle \lnot \lnot P}$${\displaystyle P}$${\displaystyle \lnot (\forall xP(x))}$${\displaystyle \exists x\lnot P(x)}$${\displaystyle \lnot (\exists xP(x))}$${\displaystyle \forall x\lnot P(x)}$${\displaystyle \lnot }$
2. 変数を標準化する
   1. 同じ変数名を 2 回使用する のような文では、変数の 1 つの名前を変更します。これにより、後で量指定子を削除するときに混乱を避けることができます。たとえば、は に名前が変更されます。${\displaystyle (\forall xP(x))\lor (\exists xQ(x))}$${\displaystyle \forall x[\exists y\mathrm {Animal} (y)\land \lnot \mathrm {Loves} (x,y)]\lor [\exists y\mathrm {Loves} (y,x)]}$${\displaystyle \forall x[\exists y\mathrm {Animal} (y)\land \lnot \mathrm {Loves} (x,y)]\lor [\exists z\mathrm {Loves} (z,x)]}$
3. 声明 をスコレム化する
   1. 量指定子を外側に移動します。繰り返して に置き換えます。 に置き換えます。に置き換えます。 に置き換えます。 に置き換えます。 前の変数標準化手順でが に出現しないことが保証されているため、これらの置き換えでは同等性が保持されます。これらの置き換えの後、量指定子は数式の最初のプレフィックスにのみ出現し、 、 、または の内側には出現しません。${\displaystyle P\land (\forall xQ(x))}$${\displaystyle \forall x(P\land Q(x))}$${\displaystyle P\lor (\forall xQ(x))}$${\displaystyle \forall x(P\lor Q(x))}$${\displaystyle P\land (\exists xQ(x))}$${\displaystyle \exists x(P\land Q(x))}$${\displaystyle P\lor (\exists xQ(x))}$${\displaystyle \exists x(P\lor Q(x))}$${\displaystyle x}$${\displaystyle P}$${\displaystyle \lnot }$${\displaystyle \land }$${\displaystyle \lor }$
   2. を で繰り返し置き換えます。ここで は新しい-ary 関数記号、いわゆる「スコーレム関数」です。これは、同値性ではなく充足可能性のみを保持する唯一のステップです。これにより、すべての存在量指定子が削除されます。${\displaystyle \forall x_{1}\ldots \forall x_{n}\;\exists y\;P(y)}$${\displaystyle \forall x_{1}\ldots \forall x_{n}\;P(f(x_{1},\ldots ,x_{n}))}$${\displaystyle f}$${\displaystyle n}$
4. すべての全称量指定子を削除します。
5. OR を AND の上に内側に分散します。繰り返しに置き換えます。${\displaystyle P\lor (Q\land R)}$${\displaystyle (P\lor Q)\land (P\lor R)}$

例

たとえば、「すべての動物を愛する人は、今度は誰かに愛される」という式は、次のように CNF に変換されます (最後の行では節形式に変換されます) (内の置換規則のredex を強調表示)。 ${\displaystyle {\color {red}{\text{red}}}}$

非公式には、スコーレム関数は、愛されている人物を返し、愛していない動物（もしあれば）を返すものと考えることができます。下の最後から 3 行目は、 「は動物を愛していない、またはに愛されている」と読めます。 ${\displaystyle g(x)}$${\displaystyle x}$${\displaystyle f(x)}$${\displaystyle x}$${\displaystyle x}$${\displaystyle f(x)}$${\displaystyle x}$${\displaystyle g(x)}$

上から2番目の最後行がCNFです。 ${\displaystyle (\mathrm {Animal} (f(x))\lor \mathrm {Loves} (g(x),x))\land (\lnot \mathrm {Loves} (x,f(x))\lor \mathrm {Loves} (g(x),x))}$

• 代数正規形
• 結合と分離の二重性
• 選言正規形
• ホーン節– ホーン節は、最大 1 つの正の、つまり否定されていないリテラルを含む選言節(リテラルの選言) です。
• クワイン・マクラスキーアルゴリズム

• 「連言正規形」、数学百科事典、EMS Press、2001 [1994]

• 「真理値表をCNFとDNFに変換するJavaツール」。マールブルク大学。 2023年12月31日閲覧。