自动认识逻辑

自动认识逻辑的语法通过增加指示知识的模态算子 ${\displaystyle \Box }$  而扩展了命题逻辑: 如果 ${\displaystyle F}$  是一个公式，则 ${\displaystyle \Box F}$  指示 ${\displaystyle F}$  是已知。作为结果，${\displaystyle \Box \neg F}$  指示 ${\displaystyle \neg F}$  是已知，而 ${\displaystyle \neg \Box F}$  指示 ${\displaystyle F}$  是未知。

在自动认识逻辑中的公式可以用来捕获基于事实知识的推理。例如，${\displaystyle \neg \Box F\rightarrow \neg F}$  意味着如果不知道 ${\displaystyle F}$  是真的，则假定它为假。这是一种形式的否定为失败。

自动认识逻辑的语义基于的是理论的展开(expansion)，它扮演的角色类似于命题逻辑中的模型。命题模型指定原子哪个为真哪个为假，而展开指定公式 ${\displaystyle \Box F}$  哪个为真哪个为假。特别是，自动认识公式 ${\displaystyle T}$  的展开对在 ${\displaystyle T}$  中包含的所有子公式 ${\displaystyle \Box F}$  都做这种区分。这种区分允许 ${\displaystyle T}$  被作为命题公式处理，因为包含 ${\displaystyle \Box }$  的所有子公式都要么是真要么是假。特别是，使用命题演算的规则来检查 ${\displaystyle T}$  在这种条件下是否蕴涵 ${\displaystyle F}$ 。为了使初始假定是一个展开，一个子公式 ${\displaystyle F}$  被蕴涵是必须的当且仅当 ${\displaystyle \Box F}$  已经被初始假定为真。

例如，在公式 ${\displaystyle T=\Box x\rightarrow x}$  中，只有一个单一的“加方框的子公式” ${\displaystyle \Box x}$ 。所以只有两个候选的展开，分别是假定它为真或为假。对实际上的展开所做的检查如下：

${\displaystyle \Box x}$  为假: 通过这个假定，因为 ${\displaystyle \Box x\rightarrow x}$  等价于 ${\displaystyle \neg \Box x\vee x}$ ，而 ${\displaystyle \neg \Box x}$  被假定为真，${\displaystyle T}$  成为重言式；所以 ${\displaystyle x}$  没有被蕴涵。这个结果符合在 ${\displaystyle \Box x}$  为假中所暗含的假定，就是说 ${\displaystyle x}$  当前是未知的。所以 ${\displaystyle \Box x}$  为假的假定是一个展开。

${\displaystyle \Box x}$  为真: 通过这个假定，${\displaystyle T}$  蕴涵 ${\displaystyle x}$ ；所以在 ${\displaystyle \Box x}$  为真中所暗含的初始假定，就是说 ${\displaystyle x}$  为真是已知的，被满足了。作为结果，这是另一个展开。

因此公式 ${\displaystyle T}$  有两个展开，在其中一个中 ${\displaystyle x}$  是未知，在另一个中 ${\displaystyle x}$  是已知。第二个被认为是反直觉的，因为 ${\displaystyle \Box x}$  为真的初始假定只说明了为什么 ${\displaystyle 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.