融合法

命題論理の意味論の課は、妥当性と充足可能性が真理値表によって決定可能であることを示した。そのコストは変数が一つ増えるごとに二倍になる。そして真理値表全体をたどる必要のない方法を予告した。意味論的帰結と同値の課は、あらゆる帰結を充足不能性に帰着させた。$\Gamma \models \varphi$ であるのは、$\Gamma \cup \{\neg\varphi\}$ が充足不能であるとき、かつそのときに限る。標準形の課とそのアルゴリズムの課は、あらゆる論理式に連言形を与えた。その妥当性は一目でわかるが、充足可能性はわからない。そうであるならば、節の連言の充足不能性を、節そのものの上で操作して判定する手続きが欠けている。その手続きが融合法である。これはジョン・アラン・ロビンソンが 1965 年に、マーティン・デイヴィスとヒラリー・パトナム（1960）の着想をもとに提案したものであり、今日、数百万の変数をもつ論理式の充足可能性を判定するプログラムの中核である。演繹の単元の体系（その意味論との関係は健全性と完全性の課とコンパクト性定理の課が調べる）とは異なり、融合法は結論を演繹しない。集合を反駁するのである。この課は、融合法がそれを健全かつ完全に行うことを証明する。

これまでの課と同様に、$p$、$q$、$r$、$s$、$t$ は変数 $v_1$ から $v_5$ を表す。添字のない文字 $v$、および $w$ は付値を表す。$V(\varphi)$ は $\varphi$ の変数の集合である。

節と節の集合

標準形の課を思い出そう。リテラルとは変数または変数の否定であり、リテラル $\ell$ の反対は $\ell^{*}$ と書かれ、同じ変数で符号が逆のリテラルである。互いに反対の二つのリテラルは相補対をなす。リテラルの否定の補題により、$v(\ell^{*}) = 1 - v(\ell)$ がすべての付値 $v$ について成り立つ。そこでは節はリテラルの選言であった。ここでは、値を変えない順序と繰り返しを忘れ、集合だけを残すのがよい。

節とはリテラルの有限集合である。リテラルをもたない節は空節と呼ばれ、$\Box$ と書かれる。付値 $v$ が節 $C$ を充足するとは（$v \models C$ と書く）、$C$ のあるリテラルが値 $1$ をとる（$v$ において）ことをいう。そうでなければ、$v$ はそれを反駁する。リテラルを一つだけもつ節は単位節と呼ばれる。節の変数は集合 $V(C)$ をなす。節の集合 $S$ の変数は集合 $V(S)$ をなし、これは前者の和集合である。付値が節の集合 $S$ を充足するとは（$v \models S$）、そのすべての節を充足することをいう。$S$ は、ある付値がそれを充足するとき充足可能であり、そうでないとき充足不能である。最後に、$S$ が節の集合で $C$ が節であるとき、$S \models C$ は、$S$ を充足するすべての付値が $C$ を充足することを意味する。

定義から二つの極端な場合が従い、それを確認しておくのがよい。空節はリテラルをもたない。したがって、そのどのリテラルも $1$ をとらず、どの付値もそれを充足しない。$\Box$ は充足不能であり、それを含むすべての集合もそうである。これに対して、節の空集合には充足すべき節がなく、すべての付値がそれを充足する。両者を混同してはならない。$\{\Box\}$ は充足不能であり、$\emptyset$ はすべての付値によって充足される。

相補対を含む節は恒真な節と呼ばれる。それは何の条件も課さず、どの集合からもそのモデルを変えずに取り除くことができる。節を集合として書くのは記法の気まぐれではない。$(p \vee q)$ と $(p \vee \neg q)$ から $p$ を得たいとき、選言は $(p \vee p)$ を与え、これは $p$ と同値であるが同じ論理式ではない。集合では $\{p\} \cup \{p\} = \{p\}$ となり、繰り返されたリテラルの融合はひとりでに起こる。