論理式の標準形
Contents
論理式の標準形
標準形 (normal form) とは、ある式を表すときに「標準」として用いられる形式のこと。形式を制限することで、式の意味や性質が解釈しやすくなる。論理式の標準形として、連言標準形 (英：conjunctive normal form, CNF) と選言標準形 (英：disjunctive normal form, DNF) を記す。連言標準形と選言標準形は、論理結合子を除き、形式が一致している。
リテラル：
リテラル (英：literal) とは、命題変項、もしくは命題変更に否定論理結合子が一つだけついた論理式。
節：
節 (clause) とは、リテラルを特定の論理結合子によって結合した論理式。
連言標準形
連言標準形とは、節の論理結合子を選言にし、連言論理結合子で結合した論理式のこと。
連言標準形の節：
\[ \bigvee_i^n l_i \equiv l_1\lor\cdots\lor l_n \]
連言標準形の定義：
\[ \bigwedge_j^m\bigvee_i^n l_{ij} \equiv \bigvee_i^n l_{i1}\land\cdots\land\bigvee_i^n l_{im} \]
選言標準形
選言標準形とは、節の論理結合子を連言にし、選言論理結合子で結合した論理式のこと。
選言標準形の節：
\[ \bigwedge_i^n l_i \equiv l_1\land\cdots\land l_n \]
選言標準形の定義：
\[ \bigvee_j^m\bigwedge_i^n l_{ij} \equiv \bigwedge_i^n l_{i1}\lor\cdots\lor\bigwedge_i^n l_{im} \]
論理式の標準形の双対性
双対性 (duality) とは、二つの記法が同じ対象を表す性質。連言標準形と選言標準形は論理結合子において互いに双対である。
\[ \lnot\bigwedge_j^m\bigvee_i^n l_{ij} \equiv \bigvee_j^m \bigwedge_i^n \lnot l_{ij} \]
導出：
ド・モルガンの定理から、
\[ \begin{aligned} \bigwedge_i^n \lnot l_i & \equiv \lnot l_1\land \lnot l_2\land \lnot l_3\land\cdots\land \lnot l_n \cr & \equiv \lnot(l_1\lor l_2)\land\lnot l_3\land\cdots\land \lnot l_n \cr & \equiv \lnot(l_1\lor l_2\lor l_3)\land\cdots\land \lnot l_n \cr & \equiv \lnot\bigvee_i^n l_i \end{aligned} \]
同値関係からを得られる真偽値を $L$ とし、それぞれの標準形を求めると、双対性を示す論理式が得られる。
\[ \begin{aligned} L \equiv \bigwedge_i \lnot l_i &\equiv \lnot\bigvee_i l_i \cr \bigwedge_j^m \lnot L_j &\equiv \lnot\bigvee_j^m L_j \cr \bigwedge_j^m\left(\lnot\lnot\bigvee_i^n l_{ij}\right) &\equiv \lnot\bigvee_j^m \bigwedge_i^n \lnot l_{ij} \cr \lnot\bigwedge_j^m\bigvee_i^n l_{ij} &\equiv \bigvee_j^m \bigwedge_i^n \lnot l_{ij} \cr \cr \therefore \lnot\bigwedge_j^m\bigvee_i^n l_{ij} &\equiv \bigvee_j^m \bigwedge_i^n \lnot l_{ij} \end{aligned} \]