自動認識邏輯

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

語法

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

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

語義

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

例如，在公式 $T=\Box x\rightarrow x$ 中，只有一個單一的“加方框的子公式” $\Box x$ 。所以只有兩個候選的展開，分別是假定它為真或為假。對實際上的展開所做的檢查如下：

$\Box x$ 為假: 通過這個假定，因為 $\Box x\rightarrow x$ 等價於 $\neg \Box x\vee x$ ，而 $\neg \Box x$ 被假定為真， $T$ 成為重言式；所以 $x$ 沒有被蘊涵。這個結果符合在 $\Box x$ 為假中所暗含的假定，就是說 $x$ 當前是未知的。所以 $\Box x$ 為假的假定是一個展開。

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

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

參見

引用

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.