デービス・パトナムのアルゴリズム
デービス・パトナムのアルゴリズム(英: Davis–Putnam algorithm)は、与えられた論理式の充足可能性を調べるアルゴリズムで、連言標準形で表現された命題論理式を対象とする。アメリカ国家安全保障局の支援を受け、一階述語論理での定理自動証明のための方法としてマーチン・デービス(英語版)(Martin Davis)とヒラリー・パトナム(Hilary Putnam)により1958年に考案され 、一般には1960年に発表された 。 その後の改良版であるDPLLアルゴリズム(Davis-Putnam-Logemann-Loveland algorithm) のベースとなるアルゴリズムである。
なお、古い文献ではDPLLアルゴリズムのことをデービス・パトナムのアルゴリズムと呼ぶことがある。それぞれは異なった規則を使用し、正確には異なる。 1960年に提案されたデービス・パトナムのアルゴリズムが導出を使用するのに対し、1962年に提案されたDPLLアルゴリズムはバックトラックを使用する。
最初、デービス・パトナムのアルゴリズムはエルブランの定理を用いて一階述語論理式の定理を証明するための方法の一部として用いられた。エルブランの定理での証明をそのまま計算機上で実現したギルモアのアルゴリズムよりは効率的で、ギルモアのアルゴリズムがIBM 704上で21分かかっても結果が出なかった問題を容易に手計算で求めることができた。 だが、基礎例を機械的に作り出しその充足不能性を調べるやり方は、多数の無駄な論理式が生成されるため効率が非常に悪く、ギルモアのアルゴリズムと同様、一階述語論理での複雑な論理式の証明はできなかった。
その後、プラウィツ(Dag Prawitz)は、論理式を生成してからチェックするのではなく、論理式への適当な代入(単一化)によって充足不能性を調べる方法を提案し 、 デービス・パトナムの枠組みにプラウィツのアイデアを組み合わせたロビンソンの導出原理の提案へのとつながっていく。
デービス・パトナムのアルゴリズム自体もより効率のよいDPLLアルゴリズム(Davis-Putnam-Logemann-Loveland algorithm)に発展し、命題論理式の充足可能性問題を解くためのアルゴリズムとして多くの定理証明システムで使用されている。