失敗による否定のソースを表示

'''失敗による否定'''（しっぱいによるひてい、{{lang-en-short|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 \land \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 \land \mathit{not}~r</math>
:<math>q \equiv s \lor 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 \lor r</math>
:<math>\mathit{not}~q \equiv \mathit{not}~s \land \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><br>
<math>p(b) \leftarrow</math><br> 

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

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

<math>p(X) \equiv X=a \lor 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つの安定な展開 Δ<sub>1</sub> = {<math>\mathit{not}~p</math>} と Δ<sub>2</sub> = {<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> はデフォルトで成り立つ）

== 参考文献 ==
* K. Clark [1978, 1987]. [http://www.doc.ic.ac.uk/~klc/neg.html Negation as failure]. ''Readings in nonmonotonic reasoning'', Morgan Kaufmann Publishers, pages 311 - 325. 
* M. Gelfond [1987] [http://www.cs.ttu.edu/~mgelfond/papers/autoepistemic.pdf On Stratified Autoepistemic Theories] Proc. AAAI, pages 207-211.
* M. Gelfond and V. Lifschitz [1988] [http://www.cs.ttu.edu/~mgelfond/papers/stable.pdf The Stable Model Semantics for Logic Programming] Proc.   5th International Conference and Symposium on Logic Programming (R. Kowalski and K. Bowen, eds), MIT Press, pages 1070-1080.

== 外部リンク ==
* [https://www.w3.org/2004/12/rules-ws/report/ Report from the W3C Workshop on Rule Languages for Interoperability] NAF と SNAF (Scoped NAF) に関する記述あり

{{DEFAULTSORT:しつはいによるひてい}}
{{Software-stub}}

[[Category:理論計算機科学]]
[[Category:人工知能]]
[[Category:数学に関する記事]]
[[Category:論理プログラミング]]