連言標準形

Standard form of Boolean function

ブール代数では、式が 1 つ以上の節の連言である場合、その式は連言標準形( CNF ) または節標準形になります。この場合、節はリテラルの選言です。それ以外の場合は、合計の積またはOR の ANDです。

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

意味

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

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

CNF 分離分離CNF ${\displaystyle \,\to \,}$ ${\displaystyle \,\mid \,}$ ${\displaystyle \,\land \,}$

分離 リテラルリテラル分離リテラル ${\displaystyle \,\to \,}$ ${\displaystyle \,\mid \,}$ ${\displaystyle \,\lor \,}$

リテラル 変数変数 ${\displaystyle \,\to \,}$ ${\displaystyle \,\mid \,}$ ${\displaystyle \,\neg \,}$

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

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

• ${\displaystyle (A\lor \neg B\lor \neg C)\land (\neg D\lor E\lor F)}$
• ${\displaystyle (A\lor B)\land (C)}$
• ${\displaystyle (A\lor 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の中にネストされているため
• ${\displaystyle A\land (B\lor (C\lor D))}$ネストされたORは括弧なしで記述する必要があるため

CNFへの変換

古典論理では、各命題式は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})}$, ^[3]

ここで、それぞれはリテラルの連結である。^[4] ${\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{// (generalized) D.M.}}\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{// (generalized) D.M.}}\end{aligned}}}$$

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

例

命題式をCNFに変換する。^[5] ${\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相当は、その真理値表から導出できます。ここでも、式を考えてみましょう。^[5] $${\displaystyle \phi =((\lnot (p\land q))\leftrightarrow (\lnot r\uparrow (p\oplus q)))}$$

対応する真理値表は

${\displaystyle p}$	${\displaystyle q}$	${\displaystyle r}$		${\displaystyle (}$	${\displaystyle \lnot }$	${\displaystyle (p\land q)}$	${\displaystyle )}$	${\displaystyle \leftrightarrow }$	${\displaystyle (}$	${\displaystyle \lnot r}$	${\displaystyle \uparrow }$	${\displaystyle (p\oplus q)}$	${\displaystyle )}$
T	T	T			F	T		F		F	T	F
T	T	F			F	T		F		T	T	F
T	F	T			T	F		T		F	T	T
T	F	F			T	F		F		T	F	T
F	T	T			T	F		T		F	T	T
F	T	F			T	F		F		T	F	T
F	F	T			T	F		T		F	T	F
F	F	F			T	F		T		T	T	F

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への変換には、同値性ではなく充足可能性を維持することで、式のサイズが指数関数的に増加することを回避する方法があります。^{[6] [7]}これらの変換は、式のサイズを線形的に増加させることが保証されていますが、新しい変数が導入されます。例えば、上記の式は、次のように変数を追加することで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}$空でない部分集合を持つ。 ^[8] ${\displaystyle (2^{2n}-1)}$

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

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

例

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

最も長いCNFには論理和がある: ^[9] ${\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}}}$$

この式は矛盾です。または に簡略化できますが、これらも矛盾であり、有効なCNFでもあります。 ${\displaystyle (\neg p\land p)}$ ${\displaystyle (\neg q\land q)}$

計算の複雑さ

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

この場合の典型的な問題は、「3CNF」と呼ばれる連言正規形の式です。これは、連言ごとに3つ以下の変数を持つ連言正規形です。実際に遭遇するこのような式の例は、例えば10万個の変数と100万個の連言を持つなど、非常に大規模になることがあります。

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式は

${\displaystyle (}$

${\displaystyle l_{11}}$

${\displaystyle \lor }$

${\displaystyle \ldots }$

${\displaystyle \lor }$

${\displaystyle l_{1n_{1}}}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \ldots }$

${\displaystyle \land }$

${\displaystyle (}$

${\displaystyle l_{m1}}$

${\displaystyle \lor }$

${\displaystyle \ldots }$

${\displaystyle \lor }$

${\displaystyle l_{mn_{m}}}$

${\displaystyle )}$

[11]は、一般的に集合の集合として表現される。

${\displaystyle \{}$

${\displaystyle \{}$

${\displaystyle l_{11}}$

${\displaystyle ,}$

${\displaystyle \ldots }$

${\displaystyle ,}$

${\displaystyle l_{1n_{1}}}$

${\displaystyle \}}$

${\displaystyle ,}$

${\displaystyle \ldots }$

${\displaystyle ,}$

${\displaystyle \{}$

${\displaystyle l_{m1}}$

${\displaystyle ,}$

${\displaystyle \ldots }$

${\displaystyle ,}$

${\displaystyle l_{mn_{m}}}$

${\displaystyle \}}$

${\displaystyle \}}$

。

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

一階述語論理からの変換

第一階論理をCNFに変換するには： ^[12]

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. whichのような文で同じ変数名が2回使われている場合は、どちらか一方の変数名を変更しましょう。こうすることで、後で量指定子を削除する際に混乱を避けることができます。例えば、は に名前が変更されます。 ${\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. を繰り返し で置き換えます。ここで は新しい- 項関数記号、いわゆる「スコーレム関数」です。これは、同値性ではなく充足可能性のみを保持する唯一のステップです。これにより、すべての存在量指定子が除去されます。 ${\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}}}}$

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \forall y}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \color {red}\rightarrow }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \rightarrow }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \forall y}$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \color {red}\rightarrow }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

1.1倍

${\displaystyle \forall x}$

${\displaystyle \color {red}\lnot }$

${\displaystyle (}$

${\displaystyle {\color {red}{\forall y}}}$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

1.1倍

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \exists y}$

${\displaystyle \color {red}\lnot }$

${\displaystyle (}$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

1.2倍

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \exists y}$

${\displaystyle \color {red}\lnot }$

${\displaystyle \color {red}\lnot }$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle (}$

${\displaystyle \exists }$

${\displaystyle y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

1.2倍

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle {\color {red}{\exists y}}}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle (}$

${\displaystyle \color {red}\exists }$

${\displaystyle \color {red}y}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle y}$

${\displaystyle ,x)}$

${\displaystyle )}$

1.2倍

${\displaystyle \forall x}$

${\displaystyle (}$

${\displaystyle \exists y}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle (}$

${\displaystyle \color {red}\exists }$

${\displaystyle \color {red}z}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle z}$

${\displaystyle ,x)}$

${\displaystyle )}$

2倍

${\displaystyle \forall x}$

${\displaystyle \exists z}$

${\displaystyle (}$

${\displaystyle {\color {red}{\exists y}}}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle z}$

${\displaystyle ,x)}$

3.1まで

${\displaystyle \forall x}$

${\displaystyle {\color {red}{\exists z}}}$

${\displaystyle \exists y}$

${\displaystyle (}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle z}$

${\displaystyle ,x)}$

3.1まで

${\displaystyle \forall x}$

${\displaystyle {\color {red}{\exists y}}}$

${\displaystyle (}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle \land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle y}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \lor }$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle g(x)}$

${\displaystyle ,x)}$

3.2倍

${\displaystyle (}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle f(x)}$

${\displaystyle )}$

${\displaystyle \color {red}\land }$

${\displaystyle \lnot }$

${\displaystyle \mathrm {Loves} (x,}$

${\displaystyle f(x)}$

${\displaystyle )}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle g(x)}$

${\displaystyle ,x)}$

4時までに

${\displaystyle (}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle f(x)}$

${\displaystyle )}$

${\displaystyle \color {red}\lor }$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle g(x)}$

${\displaystyle ,x)}$

${\displaystyle )}$

${\displaystyle \color {red}\land }$

${\displaystyle (}$

${\displaystyle \lnot \mathrm {Loves} (x,f(x))}$

${\displaystyle \color {red}\lor }$

${\displaystyle \mathrm {Loves} (g(x),x)}$

${\displaystyle )}$

5までに

${\displaystyle \{}$

${\displaystyle \{}$

${\displaystyle \mathrm {Animal} (}$

${\displaystyle f(x)}$

${\displaystyle )}$

${\displaystyle ,}$

${\displaystyle \mathrm {Loves} (}$

${\displaystyle g(x)}$

${\displaystyle ,x)}$

${\displaystyle \}}$

${\displaystyle ,}$

${\displaystyle \{}$

${\displaystyle \lnot \mathrm {Loves} (x,f(x))}$

${\displaystyle ,}$

${\displaystyle \mathrm {Loves} (g(x),x)}$

${\displaystyle \}}$

${\displaystyle \}}$

（節表現）

非公式には、スコーレム関数は、愛されている人物を返し、愛していない動物（もしいれば）を返すものと考えることができます。つまり、下の最後から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 つの正の、つまり否定されていないリテラルを持つ選言節(リテラルの選言) です。
• クワイン・マクラスキーアルゴリズム

注記

1. ハウソン 2005、46ページ。
2. 選言正規形を参照§ DNFへの変換
3. 接続詞の最大数 ${\displaystyle 1\leq m\leq }$ ${\displaystyle \phi }$
4. リテラルの最大数 ${\displaystyle 1\leq in_{i}\leq }$ ${\displaystyle \phi }$
5. = (( NOT (p AND q)) IFF (( NOT r) NAND (p XOR q))) ${\displaystyle \phi }$
6. ツェティン 1968.
7. ジャクソン＆シェリダン 2004.
8. ${\displaystyle \left|{\mathcal {P}}(L)\right|=2^{2n}}$
9. および の交換法則および結合法則に基づく繰り返しや変化 ( など)は発生しないと仮定します。 ${\displaystyle (a\land b)\lor (b\land a)\lor (a\land b\land b)}$ ${\displaystyle \lor }$ ${\displaystyle \land }$
10. CNFの充足可能性をチェックする一つの方法は、それをDNFに変換することであり、その充足可能性は線形時間でチェックできる。
11. 論理和の最大数リテラルの最大数 ${\displaystyle 1\leq m\leq }$
    ${\displaystyle 1\leq in_{i}\leq }$
12. Russel & Norvig 2010、pp. 345–347、9.5.1 第一階述語論理の連言正規形。

参考文献

• アンドリュース、ピーター・B. (2013). 『数理論理学と型理論入門：証明を通して真理へ』 シュプリンガー. ISBN 978-9401599344。
• ハウソン、コリン（2005年10月11日）[1997]. 木による論理：記号論理入門. ラウトレッジ. ISBN 978-1-134-78550-6。
• ポール・ジャクソン、ダニエル・シェリダン (2004年5月10日)。「ブール回路の節形式変換」(PDF)。ホルガー・H・フース、デイビッド・G・ミッチェル編著。「充足可能性テストの理論と応用」。充足可能性テストの理論と応用に関する第7回国際会議、SAT。改訂選集。コンピュータサイエンス講義ノート。第3542号。バンクーバー、ブリティッシュコロンビア州、カナダ：シュプリンガー 2005年。pp.  183– 198。doi : 10.1007/11527695_15。ISBN 978-3-540-31580-3。
• クライネ・ビューニング、ハンス、レットマン、テオドール（1999年8月28日）『命題論理：演繹とアルゴリズム』ケンブリッジ大学出版局、ISBN 978-0-521-63017-7。
• ラッセル、スチュアート、ノーヴィグ、ピーター編 (2010) [1995]. 『人工知能：現代的アプローチ』（PDF）（第3版）. アッパーサドルリバー、ニュージャージー州: プレンティス・ホール. ISBN 978-0-13-604259-42017年8月31日時点のオリジナルよりアーカイブ（PDF） 。
• グリゴリー・S・ツィティン（1968年）「命題計算における導出の複雑さについて」（PDF）。スリセンコ・AO（編）『構成的数学と数理論理学における構造、第2部、数学セミナー』（ロシア語からの翻訳）。ステクロフ数学研究所。pp.  115– 125。
• ホワイトシット、J.エルドン（2012年5月24日）[1961]. ブール代数とその応用. クーリエ社. ISBN 978-0-486-15816-7。

外部リンク

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

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

Retrieved from "https://en.wikipedia.org/w/index.php?title=Conjunctive_normal_form&oldid=1315831727"