節標準形

節標準形（英: Clausal normal form、CNF）とは、数理論理学において、論理プログラミングや多くの自動定理証明系で使われる論理式の標準形式である。論理式を節標準形に変換すると論理式の構造が破壊される。また、Tseitin transformation を使用せずに単純な変換をすると式のサイズが最悪ケースでは指数関数的に増大する。

変換手順

古典的な一階述語論理の論理式を節標準形に変換する手順は以下の通りである。

論理式を否定標準形にする。
スコーレム化 -- 外から内に向かって、存在量化変項をスコーレム定数に置き換え、全称量化変項をスコーレム関数に置き換えていく。具体的には次のような置換を行う。
- $\forall x P (x)$ を $\exists c P (c)$ とする。ここで $c$ は新規導入。
- $\forall x \exists y P (y)$ を $, \forall x P (f_{c} (x))$ とする。ここで $f_{c}$ は新規導入。
全称量化子を削除する。
論理式を連言標準形にする。
C1∧...∧Cn を {C1,...,Cn} に置換。それぞれの論理積は ¬A1∨...∨¬Am∨B1∨...∨Bn という形式になり、これは (A1∧...∧Am)→(B1∨...∨Bn) と等価である。
- m=0 かつ n=1 なら、Prolog における事実となる。
- m>0 かつ n=1 なら、Prolog における規則となる。
- m>0 かつ n=0 なら、Prolog におけるクエリとなる。
最後に各論理積 $(A 1 \land . . . \land A m) \to (B 1 \lor . . . \lor B n)$ を ${A 1 \land . . . \land A m \to B 1, A 1 \land . . . \land A m \to B 2, . . ., A 1 \land . . . \land A m \to B n}$ に置換する。

n = 1 の場合をホーン節と呼び、これは万能チューリング機械と同等の計算能力を有する。

完全な等価でなくとも、同等（equisatisfiable）な節標準形で十分であることが多い。その場合、指数関数的増大を防ぐには、Tseitin transformation を使用し、定義（definitions）を導入して論理式の一部を改名（rename）すればよい。