節標準形
古典的な一階述語論理の論理式を節標準形に変換する手順は以下の通りである。
論理式を否定標準形にする。
スコーレム化 -- 外から内に向かって、存在量化変項をスコーレム定数に置き換え、全称量化変項をスコーレム関数に置き換えていく。具体的には次のような置換を行う。 ∀ x P ( x ) {\displaystyle \forall x\,P(x)} を ∃ c P ( c ) {\displaystyle \exists c\,P(c)} とする。ここで c {\displaystyle c} は新規導入。 ∀ x ∃ y P ( y ) {\displaystyle \forall x\exists y\,P(y)} を , ∀ x P ( f c ( x ) ) {\displaystyle ,\forall x\,P(f_{c}(x))} とする。ここで f c {\displaystyle f_{c}} は新規導入。
全称量化子を削除する。
論理式を連言標準形にする。
C 1 ∧ . . . ∧ C n {\displaystyle C1\wedge ...\wedge Cn} を { C 1 , . . . , C n } {\displaystyle \{C1,...,Cn\}} に置換。それぞれの論理積は ¬ A 1 ∨ . . . ∨ ¬ A m ∨ B 1 ∨ . . . ∨ B n {\displaystyle \neg A1\vee ...\vee \neg Am\vee B1\vee ...\vee Bn} という形式になり、これは ( A 1 ∧ . . .