失敗による否定（しっぱいによるひてい、）は、論理プログラミングで使われる非単調論理的推論規則であり、formula_1 を導出することに失敗したとき formula_2 を自動的に導出することである。Planner や Prolog の初期から論理プログラミングの重要な機能となっている。Prolog では、論理構成要素の範囲外として実装されることが多い。純粋な Prolog では、formula_2 という形式で表される NAF リテラルは節本体に現れ、他の NAF リテラルを導出するのに使われる。例えば、次のような4つの節があるとする。NAF によれば、formula_8、formula_9、formula_1 が導出される。NAF の意味論は未解決の問題だったが、Keith Clark (1978) によって論理プログラムの完全性 (completion) の観点で正しいことが示された。大まかに言えば formula_11 は同値すなわち "formula_12" と解釈される。例えば、上記の4つの節の完全性は次のように表される。推論規則としての NAF は完全性による明示的な推論をシミュレートする。ここで等式の両辺が否定され、右辺の否定が原子論理式にまで分配される。例えば、formula_2 であることを示すには、NAF は上記等式群に関する次の推論をシミュレートする。命題論理的でない場合、別の名を持つ個体項は別の項であるという前提を形式化するため、完全性は等価性公理にまで敷衍される必要がある。NAF ではこれをユニフィケーションの失敗でシミュレートする。例えば、次の2つの節だけがあるとする。formula_24
formula_25
NAF によれば、ここから formula_26 が導出される。プログラムの完全性は次のようになる。formula_27ここでは、単一名公理と領域閉包公理によって敷衍されている。完全性意味論はサーカムスクリプションと閉世界仮説に密接に関連している。完全性意味論は、NAF 推論の結果 formula_2 を古典的な formula_1 の否定 formula_30 として解釈する。しかし、Michael Gelford (1987) では、formula_2 を自己認識論理において「formula_1 を示すことができない」、あるいは「formula_1 は未知である」、あるいは「formula_1 は信じられていない」と解釈することも可能であるとした。自己認識的解釈は、さらに Gelford と Lifschitz (1988) で研究が進み、解集合プログラミングの基盤となった。NAF リテラルを含む純粋 Prolog のプログラム P の自己認識意味論は、基底（変数を伴わない）NAF リテラルの集合 Δ を使った P の「展開; expanssion」で得られ、これは安定モデル意味論で次のような意味を持つ。言い換えれば、何が示せないかに関する前提の集合 Δ が安定であることは、Δによって展開されたプログラム P から真であることを示せない全ての文の集合が Δ であることと同値である。ここで、純粋 Prolog プログラムの文法は単純であるため、「含意」は単にモーダスポネンスと普遍例化のみで導出されるものと解釈される。プログラムはゼロか1つ以上の安定な展開を持つことができる。例えば、は安定な展開を持たない。は、1つの安定な展開 Δ = {formula_39} を持つ。は、2つの安定な展開 Δ = {formula_2} と Δ = {formula_39} を持つ。NAF の自己認識的解釈は古典的な否定と結合でき、論理プログラミングや解集合プログラミングでそのような拡張がなされている。そのような結合をすると、次のような表現が可能となる。

出典:wikipedia