連言標準形

与えられた命題論理式のCNF相当値を計算するアルゴリズム${\displaystyle \phi }$を基盤として構築する${\displaystyle \lnot \phi }$選言標準形（DNF）の場合：ステップ1. ^{[ 2 ]} 次に${\displaystyle \lnot \phi _{DNF}}$変換される$\displaystyle \phi _{CNF}}$すべてのリテラルを否定しながら、ANDとORを逆に入れ替えます。${\displaystyle \lnot \lnot }$[ ^{1 ]​}

すべての命題論理式は連言標準形（CNF）の同値な論理式に変換できるため、証明はしばしばすべての論理式が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}).}$$

解釈がこの式を満たすのは、新しい変数のうち少なくとも１つが真である場合に限る。この変数が${\displaystyle Z_{i}}$すると両方とも${\displaystyle X_{i}}$そして${\displaystyle Y_{i}}$も同様に真である。これは、この式を満たすすべてのモデルが元の式も満たすことを意味する。一方、元の式のモデルのうち、この式を満たすのは一部だけである。${\displaystyle Z_{i}}$は元の式には記載されておらず、その値は式の充足とは無関係ですが、最後の式ではそうではありません。つまり、元の式と翻訳結果は等充足可能ではありますが、同等ではありません。

別の翻訳であるツェイティン変換では、以下の節も含まれています。${\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}}$。

一階述語論理を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. 次のような文の場合${\displaystyle (\forall xP(x))\lor (\exists xQ(x))}$同じ変数名を2回使用している場合は、変数名を1つ変更します。これにより、後で量指定子を削除する際の混乱を回避できます。たとえば、${\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 g(x)}$は、${\displaystyle x}$愛されている一方で${\displaystyle f(x)}$動物（もしあれば）を生み出す${\displaystyle x}$愛していない。下から3行目は次のように読める。${\displaystyle x}$動物を愛していない${\displaystyle f(x)}$さもなければ${\displaystyle x}$愛されている${\displaystyle g(x)}$「。

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