否定正規形

Logical formula with NOT only on variables

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

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

意味

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

NNF	${\displaystyle \to }$	リテラル
		${\displaystyle \mid \quad }$（NNF NNF） ${\displaystyle \,\land \,}$
		${\displaystyle \mid \quad }$（NNF NNF） ${\displaystyle \,\lor \,}$
リテラル	${\displaystyle \to }$	変数
		${\displaystyle \mid \quad \neg \,}$ 変数

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

例と反例

∨ / \ ∧ D / \ ∧ ¬ / \ |A∨C / \ ¬C | B

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

${\displaystyle {\begin{aligned}&((A\lor B)\land C)\\&(A\lor \lnot B)\\&(A\land \lnot B)\\&((A\land (\lnot B\lor C))\land \lnot C)\end{aligned}}}$

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

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

${\displaystyle {\begin{aligned}(A&\to B)\\\lnot (A&\lor B)\\\lnot (A&\land B)\\\lnot (A&\lor \lnot C)\end{aligned}}}$

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

${\displaystyle {\begin{aligned}(\lnot A&\lor B)\\(\lnot A&\land \lnot B)\\(\lnot A&\lor \lnot B)\\(\lnot A&\land C)\end{aligned}}}$

NNFへの変換

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

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

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

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

参照

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

注記

1. ロビンソンとヴォロンコフ、2001、p. 204.

参考文献

• Robinson, John Alan ; Voronkov, Andrei編 (2001). Handbook of Automated Reasoning . 第1巻. MIT Press . pp. 203 ff. ISBN 0444829490。

外部リンク

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

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