失敗としての否定

失敗としての否定（略してNAF ）は、論理プログラミングにおける非単調推論規則であり、 の導出失敗から を導出する（つまり、は成立しないと仮定する）ために使用されます。 は、推論アルゴリズムの完全性、したがって形式論理システムに 応じて、の論理否定のステートメントとは異なる場合があります。${\displaystyle \mathrm {not} ~p}$${\displaystyle p}$${\displaystyle p}$${\displaystyle \mathrm {not} ~p}$${\displaystyle \neg p}$${\displaystyle p}$

失敗としての否定は、 PlannerとPrologの初期の頃から、論理プログラミングの重要な機能でした。 Prolog では、通常、これは Prolog の論理外構造を使用して実装されます。

より一般的には、この種の否定は、強い（つまり明示的、証明可能な）否定とは対照的に 、弱い否定として知られています^{[1] [2] 。}

Planner では、失敗としての否定は次のように実装できます。

if (not (goal p)), then (assert ¬p)

これは、証明するための徹底的な検索がp失敗した場合は、を主張することを意味します¬p。^[3] これは、命題がp後続の処理で「真ではない」と想定されることを意味します。ただし、Planner は論理モデルに基づいていないため、前述の論理的解釈は不明のままです。

純粋なPrologでは、形式のNAFリテラルは節の本体に出現し、他のNAFリテラルを導出するために使用できます。たとえば、4つの節のみが与えられている場合、 ${\displaystyle \mathrm {not} ~p}$

${\displaystyle p\leftarrow q\land \mathrm {not} ~r}$

${\displaystyle q\leftarrow s}$

${\displaystyle q\leftarrow t}$

${\displaystyle t\leftarrow }$

NAF は、および を導出するだけでなく、およびも導出します。 ${\displaystyle \mathrm {not} ~s}$${\displaystyle \mathrm {not} ~r}$${\displaystyle p}$${\displaystyle t}$${\displaystyle q}$

NAF のセマンティクスは 1978 年まで未解決の問題でしたが、その年にKeith Clark が、論理プログラムの完了に関して NAF が正しいことを示しました。大まかに言えば、「only」と「if and only if」と解釈され、「iff」または「」と表記されます。 ${\displaystyle \leftarrow }$${\displaystyle \equiv }$

例えば、上記の4つの節を完成すると、

${\displaystyle p\equiv q\land \mathrm {not} ~r}$

${\displaystyle q\equiv s\lor t}$

${\displaystyle t\equiv \mathrm {true} }$

${\displaystyle r\equiv \mathrm {false} }$

${\displaystyle s\equiv \mathrm {false} }$

NAF推論規則は、同値性の両辺が否定され、右辺の否定が原子式まで分配される補完 による推論を明示的にシミュレートします。たとえば、 を示すために、NAFは同値性による推論をシミュレートします。 ${\displaystyle \mathrm {not} ~p}$

${\displaystyle \mathrm {not} ~p\equiv \mathrm {not} ~q\lor r}$

${\displaystyle \mathrm {not} ~q\equiv \mathrm {not} ~s\land \mathrm {not} ~t}$

${\displaystyle \mathrm {not} ~t\equiv \mathrm {false} }$

${\displaystyle \mathrm {not} ~r\equiv \mathrm {true} }$

${\displaystyle \mathrm {not} ~s\equiv \mathrm {true} }$

命題的でないケースでは、異なる名前を持つ個体は異なるという仮定を形式化するために、等式公理で補完を拡張する必要がある。NAFはこれを単一化の失敗によってシミュレートする。例えば、2つの節だけが与えられた場合、

${\displaystyle p(a)\leftarrow }$

${\displaystyle p(b)\leftarrow t}$

NAF は を導出します。 ${\displaystyle \mathrm {not} ~p(c)}$

プログラムの完了は

${\displaystyle p(X)\equiv X=a\lor X=b}$

固有の名前公理とドメイン閉包公理が追加されました。

完了意味論は、制限と閉世界仮定の両方に密接に関連しています。

完了セマンティクスは、NAF 推論の結果を の古典的な否定として解釈することを正当化します。しかし、1987 年にMichael Gelfondは、自己認識論的論理のように、 を文字通り「示すことができない」、「知られていない」、「信じられていない」と解釈することも可能であることを示しました。自己認識論的解釈は、1988 年に Gelfond とLifschitzによってさらに発展し、回答セット プログラミングの基礎となっています。 ${\displaystyle \mathrm {not} ~p}$${\displaystyle \neg p}$${\displaystyle p}$${\displaystyle \mathrm {not} ~p}$${\displaystyle p}$${\displaystyle p}$${\displaystyle p}$

NAFリテラルを持つ純粋なPrologプログラムPの自己認識的意味論は、Pを次の意味で 安定な基底（変数なし）NAFリテラルΔの集合で「展開」することによって得られる。

Δ = { pではない| P ∪ Δ によってpは示されない}

言い換えれば、表示できないものについての仮定 Δ のセットは、 Δ が Δ によって拡張されたプログラム P から実際に表示できないすべての文の集合である場合に限り、安定しています。ここで、純粋な Prolog プログラムの構文は単純であるため、「によって暗示される」は、モーダスポネンスと普遍的インスタンス化のみを使用した導出可能性として非常に簡単に理解できます。

プログラムには、0個、1個、またはそれ以上の安定した展開が含まれることがあります。たとえば、

${\displaystyle p\leftarrow \mathrm {not} ~p}$

安定した拡張はありません。

${\displaystyle p\leftarrow \mathrm {not} ~q}$

正確に1つの安定展開Δ = {not q }を持つ

${\displaystyle p\leftarrow \mathrm {not} ~q}$

${\displaystyle q\leftarrow \mathrm {not} ~p}$

正確に2つの安定展開 Δ ₁ = {not p }とΔ ₂ = {not q }が存在します。

NAFの自己認識的解釈は、拡張論理プログラミングや解答集合プログラミングのように、古典的な否定と組み合わせることができる。この2つの否定を組み合わせると、例えば次のように表現できる。

${\displaystyle \neg p\leftarrow \mathrm {not} ~p}$ （閉世界仮説）と

${\displaystyle p\leftarrow \mathrm {not} ~\neg p}$ (デフォルトで保持されます)。${\displaystyle p}$

• 相互運用性のためのルール言語に関する W3C ワークショップのレポート。NAF および SNAF (スコープ付き否定は失敗) に関する注記が含まれています。