查看“︁自动认识逻辑”︁的源代码

'''自动认识逻辑'''是致力于形式化关于知识的表示和推理的[[形式逻辑]]。[[命题逻辑]]只能表达事实，而自动认识逻辑可以表达关于事实的知识和知识的缺乏。

==语法==

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

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

==语义==

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

例如，在公式 <math>T = \Box x \rightarrow x</math> 中，只有一个单一的&ldquo;加方框的子公式&rdquo; <math>\Box x</math>。所以只有两个候选的展开，分别是假定它为真或为假。对实际上的展开所做的检查如下：

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

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

因此公式 <math>T</math> 有两个展开，在其中一个中 <math>x</math> 是未知，在另一个中 <math>x</math> 是已知。第二个被认为是反直觉的，因为 <math>\Box x</math> 为真的初始假定只说明了为什么 <math>x</math> 为真，符合这个假定。换句话说，这是一个自支持的假定。允许这种信仰的自支持的逻辑叫做''非强根基的''，区别于在其中自支持是不可能的''强根基的''逻辑。自动认识逻辑的强根基变体存在。

==参见==
* [[非单调逻辑]]
* [[模态逻辑]]
* [[认识逻辑]]

==引用==
* 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&auml; (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.

[[Category:计算机逻辑]]