失敗による否定

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

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

${\displaystyle q\leftarrow s}$

${\displaystyle q\leftarrow t}$

${\displaystyle t\leftarrow }$

NAF によれば、${\displaystyle {\mathit {not}}~s}$、${\displaystyle {\mathit {not}}~r}$、${\displaystyle p}$ が導出される。

Summarize Timeline Fact Check

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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