節標準形のソースを表示

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

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

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

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

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

== 関連項目 ==
* [[連言標準形]]
* [[選言標準形]]
* [[否定標準形]]
* [[スコーレム標準形]]

{{logic}}

{{DEFAULTSORT:せつひようしゆんけい}}
[[Category:数理論理学]]
[[Category:形式手法]]
[[Category:数学に関する記事]]