連言標準形

連言標準形（れんげんひょうじゅんけい、英: Conjunctive normal form, CNF）は、数理論理学においてブール論理における論理式の標準化（正規化）の一種であり、選言節の連言の形式で論理式を表す。乗法標準形、主乗法標準形、和積標準形とも呼ぶ。正規形としては、自動定理証明で利用されている。

連言標準形とは ${\displaystyle l_{i,j}}$ がリテラルの時、以下の形式をした論理式のこと。

${\displaystyle \bigwedge _{i}\bigvee _{j}l_{i,j}}$

内側の選言を節（英: clause）と呼ぶ。

連言標準形では、1つ以上のリテラルの論理和を1つ以上含む論理積の形式となる。選言標準形(DNF)と同様、CNF における演算子は論理積、論理和、否定だけである。

以下の論理式は CNF の一種である。

${\displaystyle A\wedge B}$

${\displaystyle \neg A\wedge (B\vee C)}$

${\displaystyle (A\vee B)\wedge (\neg B\vee C\vee \neg D)\wedge (D\vee \neg E)}$

${\displaystyle (\neg B\vee C).}$

しかし、以下の論理式は CNF ではない。

${\displaystyle \neg (B\vee C)}$

${\displaystyle (A\wedge B)\vee C}$

${\displaystyle A\wedge (B\vee (D\wedge E)).}$

上記の3つの論理式はそれぞれ下記の3つの連言標準形の論理式と等価である。

${\displaystyle \neg B\wedge \neg C}$

${\displaystyle (A\vee C)\wedge (B\vee C)}$

${\displaystyle A\wedge (B\vee D)\wedge (B\vee E).}$

リテラル（英: literal）は、変項（命題）か変項の否定であり、否定演算子はこの形でのみ出現する。全ての変項（またはその否定）を含む論理式を標準項と呼び、特に全ての変項（またはその否定）の論理和の形式になっている項を最大項と呼ぶ。従って、最大項の論理積の形式になっている論理式は、CNF である。この形式は、真理値表で出力が「偽」となる行を最大項として取り出したものを論理積で繋いだものであり、その真理値表に対応する論理式となっている。つまり、真理値表で表されるものは全て連言標準形の論理式で表せ、組合せ回路も連言標準形で表せる。

連言標準形から節標準形を作ることができ、節標準形は導出に使われる。

計算複雑性理論における重要な問題の一種として、連言標準形の論理式を「真」にする各変項の真偽の組合せを問う問題がある。これを充足可能性問題(SAT)という。変項が3種類の 3-SAT はNP完全問題（3変項以上のSATは全てNP完全）だが、2-SAT は多項式時間で解く事が出来る。

連言標準形を論理式として見ると、充足可能性問題などの解法の一つとなる。左記の論理式の全ての充足解を求める手法として、二分決定グラフで表現し、これを圧縮することで実用的に解を導くことができる場合がある^[1]。二分決定グラフには幾つかの種類があるが、充足可能性問題や最適化問題の解法として実用的に取り扱う手法が知られている。

任意の論理式は等価な CNF に変換することができる。これを行うには、二重否定の除去、ド・モルガンの法則、分配法則といった論理的に等価な変換を使う。全ての論理式は CNF に変換できるため、証明に際して全ての論理式が CNF であることを前提とすることが多い。しかし、元の論理式によっては、CNF への変換によって論理式が極めて長大になることもある。例えば、論理式

${\displaystyle (X_{1}\wedge Y_{1})\vee (X_{2}\wedge Y_{2})\vee \dots \vee (X_{n}\wedge Y_{n})}$

を CNF に変換すると、${\displaystyle 2^{n}}$ 個の節を書き連ねることになる。実際、対応する CNF は

${\displaystyle (X_{1}\vee X_{2}\vee \cdots \vee X_{n})\wedge (Y_{1}\vee X_{2}\vee \cdots \vee X_{n})\wedge (X_{1}\vee Y_{2}\vee \cdots \vee X_{n})\wedge (Y_{1}\vee Y_{2}\vee \cdots \vee X_{n})\wedge \cdots \wedge (Y_{1}\vee Y_{2}\vee \cdots \vee Y_{n})}$

となる。この式は ${\displaystyle 2^{n}}$ 個の節があり、それぞれの節は各 ${\displaystyle i}$ について ${\displaystyle X_{i}}$ または ${\displaystyle Y_{i}}$ を含んでいる。

等価性よりも充足可能性を満たすよう CNF に変換することで、論理式のサイズの指数関数的増加を招かない変換方式もある。このような変換方式でのサイズ増加は線形であることが保証されるが、新たな変数を導入する必要がある。たとえば、上の論理式は新たな変数 ${\displaystyle Z_{1},\ldots ,Z_{n}}$ を導入することにより CNF

${\displaystyle (Z_{1}\vee \cdots \vee Z_{n})\wedge (\neg Z_{1}\vee X_{1})\wedge (\neg Z_{1}\vee Y_{1})\wedge \cdots \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}\equiv X_{i}\wedge Y_{i}}$ を新たな変数として導入したことに相当する。この論理式が満たされるとき、元の論理式も同時に満たされる。その一方で、${\displaystyle Z_{i}}$ は元の論理式では使用されていないので、各 ${\displaystyle Z_{i}}$ の値は元の論理式の値とは無関係であり、変換後の論理式においてはそうではない。つまり元の論理式と変換後の論理式は、充足可能性においては等価 (英: equisatisfiable) であるが、論理的に等価 (英: equivalent) ではない。

• 選言標準形
• リード・マラー標準形
• ホーン節
• クワイン・マクラスキー法

表 話 編 歴 論理学
関連項目 学術的領域 議論学 価値論 批判的思考 再帰理論 形式意味論 論理史 非形式論理学 計算機科学における論理学（英語版） 数理論理学 数学 メタ論理学 メタ数学 モデル理論 哲学的論理学 哲学 論理学の哲学 数学の哲学 証明論 集合論 論理学の歴史 基本概念 アブダクション 分析的と総合的の区別（英語版） 二律背反 アプリオリ 演繹 定義(内包と外延) 記述 帰納 推論 論理的帰結 論理形式（英語版） 論理的含意（英語版） 論理的真理 名前 必要十分条件 意味 パラドックス 可能世界論 前提 確率 理性 推理 参考 意味論 命題 サブスティトゥーション（英語版） 統語論（英語版） 真理 真理値 妥当性 数学記号の表
哲学的論理学 批判的思考と非形式論理学 分析 曖昧 信念 信用性（英語版） 根拠 説明 説明力（英語版） 事実 誤謬 探究 意見 節約 根拠 プロパガンダ 思慮分別（英語版） 推理 関連 修辞学 厳格 漠然（英語版） 論理学の哲学 構成主義 真矛盾主義 虚構主義（英語版） 有限主義（英語版） 形式主義 直観主義 論理的原子論（英語版） 論理主義 唯名論 プラトニック実在論（英語版） プラグマティズム 実在論
メタ論理学と超数学 カントールの定理 決定問題 チャーチのテーゼ 無矛盾性 実効的方法（英語版） 数学基礎論 ゲーデルの完全性定理 ゲーデルの不完全性定理 健全性 完全性 決定可能性 解釈 レーヴェンハイム-スコーレムの定理 メタ定理（英語版） 充足可能性 独立性（英語版） 独立 タイプとトークンの区別 使用と言及の区別
数理論理学 基幹 形式言語 構成規則 形式体系 演繹システム（英語版） 形式的証明 形式意味論 論理式 集合 元 クラス 古典論理 公理 自然演繹 推論規則 有限関係（英語版） 定理 論理的帰結 公理系 型理論 記号 統語論（英語版） 理論（英語版） 名辞論理学（英語版） 命題 推論 論証 妥当性 三段論法 反対の正方形 ベン図 命題論理とブール論理 ブール関数 命題論理 論理演算 真理値表 原子論理式 リテラル 述語論理 量化 全称記号 存在記号 一階述語論理 二階述語論理 高階述語論理 単項述語計算（英語版） 標準形 連言標準形 選言標準形 否定標準形 冠頭標準形 スコーレム標準形 節標準形 集合論 集合 空集合 数え上げ 外延 有限集合 関数 部分集合 冪集合 可算集合 帰納的集合 定義域 値域 順序対 非可算集合 モデル理論 モデル（英語版） 解釈（英語版） 超準モデル 有限モデル理論 真理値 妥当性 証明論 形式的証明 演繹システム（英語版） 形式体系 定理 論理的帰結 推論規則 統語論（英語版） 再帰理論 再帰 帰納的集合 帰納的可算集合 決定問題 チャーチ＝チューリングのテーゼ 計算可能関数 原始再帰関数 表現 真理値表 クワイン・マクラスキー法 カルノー図 存在グラフ 概念地図 オイラー図 ベン図 スパイダー図 タブローの方法 Xバー理論 構文木 構文解析
非古典論理 様相論理学 真理様相（英語版） 価値様相（英語版） 義務論理 信念様相（英語版） 認識論理 時相論理 線形時相論理 直観主義 直観論理 構成的解析（英語版） ハイディング算術（英語版） 直観主義型理論 構成的集合論（英語版） ファジィ論理 真理の程度（英語版） ファジィルール（英語版） ファジィ集合 ファジィ有限要素（英語版） ファジィ集合演算（英語版） 部分構造論理 構造規則（英語版） 適切さの論理 線形論理 矛盾許容論理 真矛盾主義 様相記述論理（英語版） 存在論 オントロジー言語（英語版）
論理学者 アンダーソン アリストテレス イブン・ルシュド イブン・スィーナー ベイン（英語版） バーワイズ（英語版） ベルナイス ブール ブーロス（英語版） カントール カルナップ チャーチ クリュシッポス カリー ド・モルガン フレーゲ ギーチ ゲンツェン ゲーデル ヒルベルト クリーネ クリプキ ライプニッツ レーヴェンハイム（英語版） ペアノ パース パトナム クワイン ラッセル シュレーダー（英語版） スコトゥス スコーレム スマリヤン タルスキ チューリング ホワイトヘッド オッカムのウィリアム ウィトゲンシュタイン ツェルメロ
カテゴリ