デービス・パトナムのアルゴリズム

デービス・パトナムのアルゴリズムは、与えられた論理式が充足可能かどうかを判断するための重要な手法であり、特に連言標準形で表現された命題論理式に焦点を当てています。このアルゴリズムは、1958年にマーチン・デービスとヒラリー・パトナムの二人によって提案され、1960年に正式に発表されました。アメリカ国家安全保障局からの支援を受けて開発されたこのアルゴリズムは、定理自動証明の分野で革命をもたらしました。

アルゴリズムの概要

デービス・パトナムのアルゴリズムは、充足可能性のチェックを効率的に行うために、特定の規則に基づいて動作します。基本的な理念は、与えられた論理式に含まれる無駄な部分を削除し、充足可能性に影響を与えないリテラルや論理式を取り扱うことです。同アルゴリズムは、論理式の導出を用いて証明可能性を確認し、エルブランの定理に基づいたアプローチを採用しています。

一階述語論理式Pの証明可能性と¬Pの充足不能性は同値関係にあり、エルブランの定理により、¬Pが充足不能であれば、有限のステップでPの証明が可能であることが示されています。しかし、このアプローチを定理自動証明に適用しようとすると、大量の命題論理式の充足不能性をチェックする必要が生じます。デービス・パトナムのアルゴリズムは、この負担を軽減し、高速な処理を実現することができます。

適用される規則

このアルゴリズムには、主に以下のような規則があります。それぞれの規則は、特定のリテラルや論理式に対して適用され、充足可能性の判断に寄与します。

1. 1リテラル規則（Unit Rule）: 1つのリテラルを含む節が存在する場合、そのリテラルを含む他の節を削除し、否定リテラルを消去します。
2. 純リテラル規則（Pure Literal Rule）: 否定と肯定の両方が存在しないリテラルがあれば、そのリテラルを含む節を削除します。
3. 原子論理式除去規則: 同一のリテラルが否定と肯定両方とも存在する場合、そのリテラルを除去します。
4. 包含規則: ある節のすべてのリテラルが他の節に含まれるとき、その節を除去します。
5. クリーンアップ規則: 否定と肯定のリテラルが同時に存在する節を削除します。

これらの規則は、リテラルを真と解釈することにより充足可能性を持つ節を削除していきます。アルゴリズムは与えられた節にこれらの規則を繰り返し適用し続け、最終的な結果を導き出すまで続けます。

結果の判定

デービス・パトナムのアルゴリズムが適用された結果が示す内容により、以下の二つの結果に分類されます。

- 節がなくなる（またはトートロジーを含む場合）、この結果は充足可能を意味します。
- 空の節が生成される場合、これは充足不能を示します。

このようにして、デービス・パトナムのアルゴリズムは、充足可能性を判定する際の強力なツールとして機能します。

歴史的背景

当初、デービス・パトナムのアルゴリズムはエルブランの定理を基にした証明手法の一部として利用されていました。計算機上で証明を実行する手法としては、農業への応用例がありましたが、効率的な計算を実現するためには多くの新たな方法が模索される必要がありました。

最終的に、このアルゴリズムは改良が進み、DPLLアルゴリズムと呼ばれるさらに高性能な手法へと進化し、現在では多くの定理証明システムで使用されています。また、これに関する研究は未だに活発に行われており、命題論理のさらなる発展に寄与しています。

例

充足不能な論理式の例

アプローチを示すために、充足不能な論理式を扱います。以下の論理式を例にとります。

ϕ = (p ∨ q ∨ ¬r) ∧ (¬q ∨ p) ∧ (¬p) ∧ (r ∨ q)

この式に対してデービス・パトナムのアルゴリズムを適用すると、最終的に矛盾が生じ、充足不能であることが明らかになります。

充足可能な論理式の例

同様に、充足可能な論理式を以下に示します。

ϕ = (s ∨ t) ∧ (¬s ∨ ¬t) ∧ (p ∨ u) ∧ (¬p ∨ u)

この式についてもアルゴリズムを適用し、最終的に充足可能であることが証明されたということができます。

デービス・パトナムのアルゴリズムは、論理式を効率的に処理する手段として、理論と実践の両面で重要な役割を果たしています。

もう一度検索