デービス・パトナムのアルゴリズム
デービス・パトナムのアルゴリズムは、初期の一階述語論理の定理自動証明システムで必要だった命題論理式の充足可能/不能のチェックを効率的に行うために考案されたもので、導出規則を含むいくつかの規則を用いることで充足可能であることが分かっている論理式を効率的に削除し、無駄な判定を省くことができる。
一般に、一階述語論理式 P の証明可能性(恒真性)は ¬P が充足不能(恒偽)かどうかと同値であり、エルブランの定理より ¬P が充足不能ならば、エルブラン領域の要素を述語論理式に代入した基礎例(エルブラン基底)の命題論理レベルの充足不能チェックにより、有限ステップで証明可能であることが分かっている。 しかしこの方法を定理自動証明に使おうとすると、多量の命題論理式の充足不能性をチェックする必要がある。デービス・パトナムのアルゴリズムはこのような処理を高速に行うことができる。
原子論理式 A と ¬A とを含む節を全て除去する。
1リテラル規則と純リテラル規則は特定のリテラルを真と解釈することによって充足可能となる節を除去する。1リテラル規則の適用によりさらに別のリテラルが削除可能になる場合は繰り返し規則を適用する。 包含規則は冗長な節を除去する。クリーンアップ規則はトートロジーを含む節の除去である。
原子論理式除去規則は命題論理での導出規則であり、1リテラル規則と純リテラル規則を適用したのちに使用する。規則は以下の式で表すことができる。上式は前提となる親節、下式はそれらから導かれる導出節(resolvent)を表す。
l ∨ P , ¬ l ∨ Q P ∨ Q {\displaystyle {\frac {l\vee P,\quad \neg l\vee Q}{P\vee Q}}}
アルゴリズムは、与えられた節の集合に対しこれらの規則を繰り返し適用し、以下の結果が求まれば停止する。
節が無くなれば(あるいはトートロジーを含む節のみになれば)、結果は充足可能
空節(リテラルを含まない節)が生じれば、結果は充足不能
デービス・パトナムのアルゴリズムについて、以下の定理が成り立つ。