第7章 標準形とエルブラン定理

連言・選言標準形

以下の議論では限量子を含むものは考えない

連言標準形

(P1 ∨ P2)∧(P3 ∨ P4)∧(P5 ∨ P6)のように、∨で結合した節(clause)を∧で結合した形。

選言標準形

(P1 ∧ P2)∨(P3 ∧ P4)∨(P5 ∧ P6)のように、∧で結合したもの（特に名前はない）を∨で結合した形。

任意の論理式は標準形論理式に変換できる。

連言標準形を求めるアルゴリズム

入力：限量子を含まない論理式A
出力：Aと意味論的同値な連言標準形論理式B
手順：プリント参照

アルゴリズムが正しいことの証明

1. どのステップも意味論的同値の関係にある
2. 連言標準形でないならばいずれかのステップが必ず実行可能である。
3. 無限の手順となることはない

冠頭標準形

限量子のない論理式の先頭に限量子が（複数でもよい）並んでいる形の論理式。

任意の論理式は冠頭標準形に変換できる。