封闭世界假定是当前不是已知的事物都为假的假定。这个名字也称呼Ray Reiter对这个假定的逻辑形式化。与封闭世界假定相对立的使用开放世界假定,宣称知识的缺乏不蕴涵虚假。

否定为失败与封闭世界假定有关,因为它总体上相信不能被证明为真的所有命题都是假的。

封闭世界假定经常暗含在数据库中,因为所有没有明确的包换在记录都暗含的假定表示这是假(而不是未知)这个事实。例如,如果数据库包含下列表,报告写作给定文章的人的,关于没有编辑形式逻辑的文章的人的查询,经常被预期返回“Sarah Johnson”。

More information 编辑, 编辑者 ...
编辑
编辑者 文章
John Doe 形式逻辑
Joshua A. Norton 形式逻辑
Sarah Johnson 空间数据库导论
Charles Ponzi 形式逻辑
Emma Lee-Choon 形式逻辑
Close

这个结果服从表中不包含Sarah在第一个位置而“形式逻辑”在第二个位置的行的事实。这个论证暗含的是基于表中缺乏“Sarah|形式逻辑”这样的行蕴涵Sarah没有编辑关于形式逻辑的文章的假定。所以,这个查询的结果基于的是封闭世界假定,与之相对,在开放世界假定中,没有明确的陈述的事物是未知的而不是假的。在开放世界假定中,Sarah编辑这个文章是未知的;在封闭世界假说中,她没有编辑这个文章是已知的。

逻辑形式化

封闭世界假定首要逻辑形式化在于向知识库增加当前不被它所蕴涵的文字。如果知识库是Horn范式的,则这种增加的结果总是相容的,但是在其他情况下就不保证了。例如,知识库

不蕴涵也不蕴涵

向知识库增加这两个文字的否定会导致

这是矛盾的。换句话说,封闭世界假定的这种形式化有时把相容的知识库转变成矛盾的。在知识库的所有Herbrand模型的交集也是的模型的时候,封闭世界假定完全不会把矛盾介入;在命题的情况下,这个条件等价于有一个单一的最小化模型,这里模型是最小化的,如果没有其他模型拥有被指派为真的这些变量的子集。

不能忍受这个问题的可供选择的形式化已经被提出了。在下列描述中,考虑的知识库被假定为是命题的。在所有情况下,封闭世界假定的形式化都是基于向增加的“自由否定”--就是说可以被假定为假的公式的否定。换句话说,封闭世界假定应用于命题公式生成公式:

的自由否定的公式集合可以用不同方式定义,这导致封闭世界假定的不同的形式化。下面是在各种形式化中是自由否定的的定义。

CWA(封闭世界假定)
是不被蕴涵的肯定文字;
GCWA(普遍CWA)
是肯定命题,使得对于的所有肯定子句成立;
EGCWA(扩展GCWA)
同上,但是肯定文字的合取;
CCWA(仔细CWA)
同于GCWA,但是只考虑肯定子句,如果它是由给定集合的肯定文字和来自其他集合的(肯定和否定二者)文字构成的;
ECWA(扩展CWA)
类似于CCWA,但是是不包含来自给定集合的文字的任意公式。

ECWA和界限的公式化在命题理论上是一致的。查询答复的复杂性(在封闭世界假定下检查一个公式是否被另一个公式所蕴涵)对于一般公式集典型的是在多项式层次中第二级中的,并且对于Horn公式范围是从PcoNP。检查最初的封闭世界假定是否介入矛盾,要求对NP oracle的最多对数次的调用,这个问题的精确的复杂性还不知道。

缺陷

如果逻辑中含有否定目标,则封闭世界假定可能会得出矛盾的结论。[1]

shaves(小米,小米)。
shaves(张师傅,X:- villager (X), not(shaves(X,X).
villager(小米)。
villager(老王)。
villager(张师傅)。

这段代码演示了罗素悖论。小米给自己理发(shaves)。张师傅是个理发师,他给村里所有不给自己理发的人理发(是否定目标)。问张师傅给不给自己理发。

  • 如果张师傅不给自己理发,那么由于张师傅是村民(villager(张师傅)),也不给自己理发(not(shaves(X,X))),所以得出结论张师傅应该给自己理发。于是得出矛盾结论。
  • 如果张师傅给自己理发,那么要求张师傅是村民(villager(张师傅)),且not(shaves(X,X))为真,即张师傅不给自己理发。于是得出矛盾结论。

参见

参考资料

外部链接

Wikiwand in your browser!

Seamless Wikipedia browsing. On steroids.

Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.

Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.