失敗による否定

提供: miniwiki
2014/12/27/ (土) 19:40時点におけるja>埊による版 (Category:論理プログラミングを追加 (HotCat使用))
(差分) ← 古い版 | 最新版 (差分) | 新しい版 → (差分)
移動先:案内、検索

失敗による否定（しっぱいによるひてい、英: Negation as failure, NAF）は、論理プログラミングで使われる非単調論理的推論規則であり、[math]p[/math] を導出することに失敗したとき [math]\mathit{not}~p[/math] を自動的に導出することである。Planner や Prolog の初期から論理プログラミングの重要な機能となっている。Prolog では、論理構成要素の範囲外として実装されることが多い。

Prolog

純粋な Prolog では、[math]\mathit{not}~p[/math] という形式で表される NAF リテラルは節本体に現れ、他の NAF リテラルを導出するのに使われる。例えば、次のような4つの節があるとする。

[math]p \leftarrow q \and \mathit{not}~r[/math]
[math]q \leftarrow s[/math]
[math]q \leftarrow t[/math]
[math]t \leftarrow[/math]

NAF によれば、[math]\mathit{not}~s[/math]、[math]\mathit{not}~r[/math]、[math]p[/math] が導出される。

完全性意味論

NAF の意味論は未解決の問題だったが、Keith Clark (1978) によって論理プログラムの完全性 (completion) の観点で正しいことが示された。大まかに言えば [math]\leftarrow[/math] は同値すなわち "[math]\equiv[/math]" と解釈される。

例えば、上記の4つの節の完全性は次のように表される。

[math]p \equiv q \and \mathit{not}~r[/math]
[math]q \equiv s \or t[/math]
[math]t \equiv \mathit{true}[/math]
[math]r \equiv \mathit{false}[/math]
[math]s \equiv \mathit{false}[/math]

推論規則としての NAF は完全性による明示的な推論をシミュレートする。ここで等式の両辺が否定され、右辺の否定が原子論理式にまで分配される。例えば、[math]\mathit{not}~p[/math] であることを示すには、NAF は上記等式群に関する次の推論をシミュレートする。

[math]\mathit{not}~p \equiv \mathit{not}~q \or r[/math]
[math]\mathit{not}~q \equiv \mathit{not}~s \and \mathit{not}~t[/math]
[math]\mathit{not}~t \equiv \mathit{false}[/math]
[math]\mathit{not}~r \equiv \mathit{true}[/math]
[math]\mathit{not}~s \equiv \mathit{true}[/math]

命題論理的でない場合、別の名を持つ個体項は別の項であるという前提を形式化するため、完全性は等価性公理にまで敷衍される必要がある。NAF ではこれをユニフィケーションの失敗でシミュレートする。例えば、次の2つの節だけがあるとする。

[math]p(a) \leftarrow[/math]
[math]p(b) \leftarrow[/math]

NAF によれば、ここから [math]\mathit{not}~p(c)[/math] が導出される。

プログラムの完全性は次のようになる。

[math]p(X) \equiv X=a \or X=b[/math]

ここでは、単一名公理と領域閉包公理によって敷衍されている。

完全性意味論はサーカムスクリプションと閉世界仮説に密接に関連している。

自己認識意味論

完全性意味論は、NAF 推論の結果 [math]\mathit{not}~p[/math] を古典的な [math]p[/math] の否定 [math]\neg p[/math] として解釈する。しかし、Michael Gelford (1987) では、[math]\mathit{not}~p[/math] を自己認識論理において「[math]p[/math] を示すことができない」、あるいは「[math]p[/math] は未知である」、あるいは「[math]p[/math] は信じられていない」と解釈することも可能であるとした。自己認識的解釈は、さらに Gelford と Lifschitz (1988) で研究が進み、解集合プログラミングの基盤となった。

NAF リテラルを含む純粋 Prolog のプログラム P の自己認識意味論は、基底（変数を伴わない）NAF リテラルの集合 Δ を使った P の「展開; expanssion」で得られ、これは安定モデル意味論で次のような意味を持つ。

Δ = {[math]\mathit{not}~p[/math] | [math]p[/math] は P ∪ Δ に含まれない}

言い換えれば、何が示せないかに関する前提の集合 Δ が安定であることは、Δによって展開されたプログラム P から真であることを示せない全ての文の集合が Δ であることと同値である。ここで、純粋 Prolog プログラムの文法は単純であるため、「含意」は単にモーダスポネンスと普遍例化のみで導出されるものと解釈される。

プログラムはゼロか1つ以上の安定な展開を持つことができる。例えば、

[math]p \leftarrow \mathit{not}~p[/math]

は安定な展開を持たない。

[math]p \leftarrow \mathit{not}~q[/math]

は、1つの安定な展開 Δ = {[math]\mathit{not}~q[/math]} を持つ。

[math]p \leftarrow \mathit{not}~q[/math]
[math]q \leftarrow \mathit{not}~p[/math]

は、2つの安定な展開 Δ1 = {[math]\mathit{not}~p[/math]} と Δ2 = {[math]\mathit{not}~q[/math]} を持つ。

NAF の自己認識的解釈は古典的な否定と結合でき、論理プログラミングや解集合プログラミングでそのような拡張がなされている。そのような結合をすると、次のような表現が可能となる。

[math]\neg p \leftarrow \mathit{not}~p[/math] （閉世界仮説）
[math]p \leftarrow \mathit{not}~\neg p[/math] （[math]p[/math] はデフォルトで成り立つ）

参考文献

外部リンク



「http:///http:///mymemo.xyz/mymemo.xyz/wiki/index.php?title=失敗による否定&oldid=112002」から取得