自动认识逻辑 - 维基百科,自由的百科全书
自动认识逻辑是致力于形式化关于知识的表示和推理的形式逻辑。命题逻辑只能表达事实,而自动认识逻辑可以表达关于事实的知识和知识的缺乏。
语法
[编辑]自动认识逻辑的语法通过增加指示知识的模态算子 而扩展了命题逻辑: 如果 是一个公式,则 指示 是已知。作为结果, 指示 是已知,而 指示 是未知。
在自动认识逻辑中的公式可以用来捕获基于事实知识的推理。例如, 意味着如果不知道 是真的,则假定它为假。这是一种形式的否定为失败。
语义
[编辑]自动认识逻辑的语义基于的是理论的展开(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.