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

1 定義

2 概要

3 脚注

4 関連項目

定義

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

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

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

以下の論理式は CNF の一種である。 A ∧ B {\displaystyle A\wedge B} ¬ A ∧ ( B ∨ C ) {\displaystyle \neg A\wedge (B\vee C)} ( A ∨ B ) ∧ ( ¬ B ∨ C ∨ ¬ D ) ∧ ( D ∨ ¬ E ) {\displaystyle (A\vee B)\wedge (\neg B\vee C\vee \neg D)\wedge (D\vee \neg E)} ( ¬ B ∨ C ) . {\displaystyle (\neg B\vee C).}

しかし、以下の論理式は CNF ではない。 ¬ ( B ∨ C ) {\displaystyle \neg (B\vee C)} ( A ∧ B ) ∨ C {\displaystyle (A\wedge B)\vee C} A ∧ ( B ∨ ( D ∧ E ) ) . {\displaystyle A\wedge (B\vee (D\wedge E)).}

上記の3つの論理式はそれぞれ下記の3つの連言標準形の論理式と等価である。 ¬ B ∧ ¬ C {\displaystyle \neg B\wedge \neg C} ( A ∨ C ) ∧ ( B ∨ C ) {\displaystyle (A\vee C)\wedge (B\vee C)} A ∧ ( B ∨ D ) ∧ ( B ∨ E ) . {\displaystyle A\wedge (B\vee D)\wedge (B\vee E).}

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

任意の論理式を CNF に変換するには、二重否定の除去、ド・モルガンの法則、分配法則といった論理的に等価な変換を行う法則を使う。全ての論理式は連言標準形に変換できる。このため、証明に際して全ての論理式が CNF であることを前提とすることが多い。しかし、元の論理式によっては、CNF への変換によって論理式が極めて長大になることもある。例えば、次の論理式を CNF に変換すると、2n 個の項を書き連ねることになる。 ( X 1 ∧ Y 1 ) ∨ ( X 2 ∧ Y 2 ) ∨ ⋯ ∨ ( X n ∧ Y n ) . {\displaystyle (X_{1}\wedge Y_{1})\vee (X_{2}\wedge Y_{2})\vee \dots \vee (X_{n}\wedge Y_{n}).}

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

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

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

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

[ヘルプ]
^ Randal E. Bryant. "Graph-Based Algorithms for Boolean Function Manipulation". IEEE Transactions on Computers, C-35(8):677?691, 1986.

関連項目

選言標準形

リード・マラー標準形

ホーン節

クワイン・マクラスキー法

表

話

編

歴
論理学

 関連項目

学術的領域議論学 - 価値論 - 批判的思考 - 再帰理論 - 形式意味論 - 論理史 - 非形式論理学 - 計算機科学における論理学 - 数理論理学 - 数学 - メタ論理学 - メタ数学 - モデル理論 - 哲学的論理学 - 哲学 - 論理学の哲学 - 数学の哲学 - 証明論 - 集合論
基本概念アブダクション - 分析的と総合的の区別 - 二律背反 - アプリオリ - 演繹 - 定義(内包と外延) - 記述 - 帰納 - 推論 - 論理的帰結 - 論理形式 - 論理的含意 - 論理的真理 - 名前 - 必要十分条件 - 意味 - パラドックス - 可能世界論 - 前提 - 確率 - 理性 - 推理 - 参考 - 意味論 - 命題 - 代用 - 統語論 - 真理 - 真理値 - 妥当性 - 数学記号の表

 哲学的論理学

批判的思考と非形式論理学分析 - 曖昧 - 信念 - 信用性 - 根拠 - 説明 - 説明力 - 事実 - 誤謬 - 探究 - 意見 - 節約 - 根拠 - プロパガンダ - 思慮分別 - 推理 - 関連 - 修辞学 - 厳格 - 漠然
論理学の哲学構成主義 - ダイアリーシズム - 虚構主義 - 有限主義 - 形式主義 - 数学的直観主義 - 論理的原子論 - 論理主義 - 唯名論 - プラトニック実在論 - プラグマティズム - 実在論