失敗による否定

失敗による否定（Negation as Failure）

失敗による否定（NAF）は、論理プログラミングの分野で使用される非単調論理的な推論規則の一つです。この手法は、ある命題の導出に失敗した場合、その否定を自動的に導出することを可能にします。具体的には、命題 "p" が得られないときに "not p" と推定される仕組みです。NAF は、Planner や Prolog などの初期の論理プログラミング言語において、重要な役割を果たしてきました。

PrologにおけるNAF

Prologの純粋な形式では、NAFリテラルは "not p" の形で表現され、節の本体内に現れます。このリテラルは他のNAFリテラルを導出するための鍵となります。次に示すのは、典型的な4つの節の例です。

1. p ← q ∧ not r
2. q ← s
3. q ← t
4. t ←

この場合、NAFの規則に基づき、次の命題が導出されます： "not s", "not r", "p"。

完全性意味論

NAFの完全性意味論は、これまでに未解決の問題でしたが、Keith Clarkによって1978年に論理プログラムの完全性の観点から示されました。大まかに言うと、Prologにおける推論は
"←"を「同値」として解釈することで表現できます。上記の4つの節の完全性は、次のようにまとめられます：

• - p ≡ q ∧ not r
• - q ≡ s ∨ t
• - t ≡ true
• - r ≡ false
• - s ≡ false

NAF の推論ルールは、これらの等式を使って明示的な推論をシミュレートします。この際、否定された命題は原子論理式に分配されます。

ユニフィケーションの失敗

論理推論において、異なる名前を持つ個体項が異なる項であるという前提を形式化するため、保持している完全性は等価性公理に基づいています。NAFはユニフィケーションの失敗をシミュレートし、例えば、簡単な2つの節がある場合、次のように導出されます：

1. p(a) ←
2. p(b) ←

この場合、NAFにより、"not p(c)" が導出されます。プログラムの完全性はこうした条件に基づいて次のように表現されます：
p(X) ≡ X=a ∨ X=b。

自己認識意味論

完全性意味論は、NAF推論の結果を古典的な論理の否定と解釈することが一般的ですが、1987年にMichael Gelfondは、"not p" を自己認識的な文脈で解釈する考えを提唱しました。この解釈に基づくと、"p"を示せない、または"p"が未知である、または"p"が信じられていないという形で認識されます。この考え方は、GelfondとLifschitzによってさらに発展し、解集合プログラミングの基礎ともなりました。

自己認識的意味論におけるNAFリテラルを含むPrologプログラムは、基底NAFリテラルの集合を用いて「展開」され、その結果として安定モデルの意味を持ちます。この展開では、文が真であることを示せない前提が安定した集合として定義されます。

まとめ

最終的に、NAFの自己認識的解釈は古典的否定と結合可能であり、論理プログラミングや解集合プログラミングにおいて多くの応用が存在します。このような結合により、実行される推論の複雑性が大幅に向上します。例えば、"¬ p ← not p" や "p ← not ¬ p" の接続がその一例です。NAFの多様な適用は、論理の理解を深め、新たな推論理論の発展に寄与しています。

もう一度検索