否定為失敗

維基百科,自由的百科全書
跳至導覽 跳至搜尋

否定為失敗是對邏輯否定做的釋義,依據公式的否定為真,若且唯若這個公式不能被證明為真。否定為失敗用於邏輯編程語言比如 Prolog

邏輯中,否定的標準解釋是公式的否定為真,若且唯若這個公式為假。如果這個公式非真非假,它的否定被當作是未知。反過來,依據否定為失敗的解釋,這個公式的否定被當作為真。

在 Prolog 中用的否定被解釋器按否定為失敗處理。假如程序執行期間,解釋器必須求值 NOT a(b),它嘗試證明 a(b) 為真。如果這個嘗試不成功,則 NOT a(b) 被當作為真。

否定為失敗與把不知道為真的東西做為假的常見預設假定有關。這叫做封閉世界假定

外部連結[編輯]

  • Report from the W3C Workshop on Rule Languages for Interoperability. Includes notes on NAF and SNAF (scoped negation as failure).