跳至內容

自動認識邏輯

維基百科,自由的百科全書

自動認識邏輯是致力於形式化關於知識的表示和推理的形式邏輯命題邏輯只能表達事實,而自動認識邏輯可以表達關於事實的知識和知識的缺乏。

語法

自動認識邏輯的語法通過增加指示知識的模態算子 而擴展了命題邏輯: 如果 是一個公式,則 指示 是已知。作為結果, 指示 是已知,而 指示 是未知。

在自動認識邏輯中的公式可以用來捕獲基於事實知識的推理。例如, 意味着如果不知道 是真的,則假定它為假。這是一種形式的否定為失敗

語義

自動認識邏輯的語義基於的是理論的展開(expansion),它扮演的角色類似於命題邏輯中的模型。命題模型指定原子哪個為真哪個為假,而展開指定公式 哪個為真哪個為假。特別是,自動認識公式 的展開對在 中包含的所有子公式 都做這種區分。這種區分允許 被作為命題公式處理,因為包含 的所有子公式都要麼是真要麼是假。特別是,使用命題演算的規則來檢查 在這種條件下是否蘊涵 。為了使初始假定是一個展開,一個子公式 被蘊涵是必須的當且僅當 已經被初始假定為真。

例如,在公式 中,只有一個單一的“加方框的子公式” 。所以只有兩個候選的展開,分別是假定它為真或為假。對實際上的展開所做的檢查如下:

為假: 通過這個假定,因為 等價於 ,而 被假定為真, 成為重言式;所以 沒有被蘊涵。這個結果符合在 為假中所暗含的假定,就是說 當前是未知的。所以 為假的假定是一個展開。

為真: 通過這個假定, 蘊涵 ;所以在 為真中所暗含的初始假定,就是說 為真是已知的,被滿足了。作為結果,這是另一個展開。

因此公式 有兩個展開,在其中一個中 是未知,在另一個中 是已知。第二個被認為是反直覺的,因為 為真的初始假定只說明了為什麼 為真,符合這個假定。換句話說,這是一個自支持的假定。允許這種信仰的自支持的邏輯叫做非強根基的,區別於在其中自支持是不可能的強根基的邏輯。自動認識邏輯的強根基變體存在。

參見

引用

  • G. Gottlob (1995). Translating default logic into standard autoepistemic logic. Journal of the ACM, 42:711-740.
  • T. Janhunen (1998). On the intertranslatability of autoepistemic, default and priority logics. In Proceedings of the Sixth European Workshop on Logics in Artificial Intelligence (JELIA'98), pages 216-232.
  • W. Marek and M. Truszczynski (1991). Autoepistemic logic. Journal of the ACM, 38(3):588-619.
  • R. C. Moore (1985). Semantical considerations on nonmonotonic logic. Artificial Intelligence, 25:75-94.
  • I. Niemelä (1988). Decision procedure for autoepistemic logic. In Proceedings of the Ninth International Conference on Automated Deduction (CADE'88), volume 310 of Lecture Notes in Computer Science, pages 675-684. Springer.