第8章 分解証明系(2)

節（Clause）

全ての要素がアトムであるシークェントのことを節という。空シークェントを空節という。

冠頭標準形：スコーレム標準形：節集合
充足不能性で等価である。
スコーレム標準形を節の集合で表したものを節形式という。

名前変代入

名前変えにより共通の自由変数をなくすことができる代入対を分離代入対という。

眠い・・・分解DAGってのはそんなに難しくないようだ。Cut規則を繰り返せばよいようだ。