否定正規形

数学的論理では、否定演算子 ( 、not ) が変数にのみ適用され、他に許可されるブール演算子が論理積( 、and ) と論理和( 、または) のみである場合、式は否定正規形 (NNF) になります。 ${\displaystyle \lnot}$${\displaystyle \land}$${\displaystyle \lor}$

否定正規形は標準形式ではありません。たとえば、と は同等であり、 は両方とも否定正規形です。 ${\displaystyle a\land (b\lor \lnot c)}$${\displaystyle (a\land b)\lor (a\land \lnot c)}$

古典論理や多くの様相論理では、含意と同値を定義に置き換え、ド・モルガンの法則を使って否定を内側に押し込み、二重否定を排除することで、あらゆる論理式をこの形式にすることができます。このプロセスは、次の書き換え規則を使用して表すことができます。^[1]

${\displaystyle {\begin{aligned}A\Rightarrow B&~\to ~\lnot A\lor B\\A\Leftrightarrow B&~\to ~(\lnot A\lor B)\land (A\lor \lnot B)\\\lnot (A\lor B)&~\to ~\lnot A\land \lnot B\\\lnot (A\land B)&~\to ~\lnot A\lor \lnot B\\\lnot \lnot A&~\to ~A\\\lnot \exists xA&~\to ~\forall x\lnot A\\\lnot \forall xA&~\to ~\exists x\lnot A\end{aligned}}}$

(これらの規則では、記号は書き換えられる式における論理的含意を示し、書き換え操作です。) ${\displaystyle \Rightarrow}$${\displaystyle \to}$

否定正規形への変換では、式のサイズは線形にのみ増加します。つまり、原子式の出現回数は同じままで、およびの出現回数の合計は変化せず、正規形での出現回数は元の式の長さによって制限されます。 ${\displaystyle \land}$${\displaystyle \lor}$${\displaystyle \lnot}$

否定正規形の式は、分配法則を適用することで、より強い連言正規形または選言正規形に変換できます。分配法則を繰り返し適用すると、式のサイズが指数関数的に増加する可能性があります。古典的な命題論理では、否定正規形への変換は計算特性に影響を与えません。つまり、充足可能性問題は引き続きNP 完全であり、妥当性問題は引き続き共 NP 完全です。連言正規形の式の場合、妥当性問題は多項式時間で解決可能であり、選言正規形の式の場合、充足可能性問題は多項式時間で解決可能です。

次の式はすべて否定正規形です。

${\displaystyle {\begin{aligned}(A&\vee B)\wedge C\\(A&\wedge (\lnot B\vee C)\wedge \lnot C)\vee D\\A&\vee \lnot B\\A&\wedge \lnot B\end{aligned}}}$

最初の例も連言正規形であり、最後の 2 つは連言正規形と選言正規形の両方ですが、2 番目の例はどちらでもありません。

次の式は否定正規形ではありません。

${\displaystyle {\begin{aligned}A&\Rightarrow B\\\lnot (A&\vee B)\\\lnot (A&\wedge B)\\\lnot (A&\vee \lnot C)\end{aligned}}}$

ただし、これらはそれぞれ、否定正規形の次の式と同等です。

${\displaystyle {\begin{aligned}\lnot A&\vee B\\\lnot A&\wedge \lnot B\\\lnot A&\vee \lnot B\\\lnot A&\wedge C\end{aligned}}}$

• 連言標準形
• 選言正規形

• Robinson, John Alan ; Voronkov, Andrei編 (2001)。自動推論ハンドブック。第 1 巻。MITプレス。203 ページ以降。ISBN 0444829490。

• 論理式を否定正規形に変換し、使用される法則を表示するJavaアプレット