自動認識邏輯

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

基本介紹

• 中文名：自動認識邏輯
• 本質：形式邏輯

語法

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

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

語義

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

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

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

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

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

參見

• 非單調邏輯
  
• 模態邏輯
  
• 認識邏輯