查看“︁封闭世界假定”︁的源代码

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

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

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

{| border="1" cellspacing="0" cellpadding="2" align="center"
! colspan="2" style="background:#ffdead;" | 编辑
|-
! style="background:#efefef;" | 编辑者
! style="background:#efefef;" | 文章
|-
| John Doe || 形式逻辑
|-
| Joshua A. Norton || 形式逻辑
|-
| Sarah Johnson || 空间数据库导论
|-
| Charles Ponzi || 形式逻辑
|-
| Emma Lee-Choon || 形式逻辑
|}

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

==逻辑形式化==

封闭世界假定首要[[逻辑]]形式化在于向知识库增加当前不被它所蕴涵的文字。如果知识库是[[Horn子句|Horn范式]]的，则这种增加的结果总是相容的，但是在其他情况下就不保证了。例如，知识库
:<math>\{English (Fred) \vee Irish (Fred)\}</math>
不蕴涵<math>English (Fred)</math>也不蕴涵<math>Irish (Fred)</math>。

向知识库增加这两个文字的否定会导致
:<math>\{English (Fred) \vee Irish (Fred), \neg English (Fred), \neg Irish (Fred)\}</math>
这是矛盾的。换句话说，封闭世界假定的这种形式化有时把相容的知识库转变成矛盾的。在知识库<math>K</math>的所有Herbrand模型的交集也是<math>K</math>的模型的时候，封闭世界假定完全不会把矛盾介入<math>K</math>；在命题的情况下，这个条件等价于<math>K</math>有一个单一的最小化模型，这里模型是最小化的，如果没有其他模型拥有被指派为真的这些变量的子集。

不能忍受这个问题的可供选择的形式化已经被提出了。在下列描述中，考虑的知识库<math>K</math>被假定为是命题的。在所有情况下，封闭世界假定的形式化都是基于向<math>K</math>增加<math>K</math>的“自由否定”--就是说可以被假定为假的公式的否定。换句话说，封闭世界假定应用于命题公式<math>K</math>生成公式：
:<math>K \wedge \{\neg f ~|~ f \in F\}</math>。
<math>K</math>的自由否定的公式集合<math>F</math>可以用不同方式定义，这导致封闭世界假定的不同的形式化。下面是在各种形式化中是自由否定的<math>f</math>的定义。

; CWA（封闭世界假定） : <math>f</math>是不被<math>K</math>蕴涵的肯定文字；

; GCWA（普遍CWA）: <math>f</math>是肯定命题，使得对于<math>K \not\models c</math>的所有肯定子句<math>c</math>，<math>T \not\models c \vee f</math>成立；

; EGCWA（扩展GCWA）:同上，但<math>f</math>是肯定文字的合取；

; CCWA（仔细CWA）:同于GCWA，但是只考虑肯定子句，如果它是由给定集合的肯定文字和来自其他集合的（肯定和否定二者）文字构成的；

; ECWA（扩展CWA）:类似于CCWA，但是<math>f</math>是不包含来自给定集合的文字的任意公式。

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

==缺陷==
如果逻辑中含有否定目标，则封闭世界假定可能会得出矛盾的结论。<ref>{{cite book|author=Carlo Zaniolo|title=Advanced Database Systems|url=https://archive.org/details/advanceddatabase00zani|year=1997|publisher=Morgan Kaufmann Publishers|isbn=1-55860-443-X|pages=[https://archive.org/details/advanceddatabase00zani/page/n193 183]}}</ref>

<syntaxhighlight lang="prolog">
shaves(小米, 小米).
shaves(张师傅, X) :- villager(X), not(shaves(X,X)).
villager(小米).
villager(老王).
villager(张师傅).
</syntaxhighlight>
这段代码演示了[[罗素悖论]]。小米给自己理髮（shaves）。张师傅是个理髮師，他给村里所有不给自己理髮的人理髮（是否定目标）。问张师傅给不给自己理髮。
* 如果张师傅不给自己理髮，那么由于张师傅是村民（villager(张师傅)），也不给自己理髮（not(shaves(X, X))），所以得出结论张师傅应该给自己理髮。于是得出矛盾结论。
* 如果张师傅给自己理髮，那么要求张师傅是村民（villager(张师傅)），且 not(shaves(X, X)) 为真，即张师傅不给自己理髮。于是得出矛盾结论。

==参见==

* [[开放世界假定]]
* [[非单调逻辑]]
* [[界限]]
* [[否定为失败]]
* [[缺省逻辑]]

==参考资料==

* M. Cadoli and M. Lenzerini (1994). The complexity of propositional closed world reasoning and circumscription. ''Journal of Computer and System Sciences'', 48:255-310.

* T. Eiter and G. Gottlob (1993). Propositional circumscription and extended closed world reasoning are <math>\Pi^p_2</math>-complete. ''Theoretical Computer Science'', 114:231-245.

* V. Lifschitz (1985). Closed-world databases and circumscription. ''Artificial Intelligence'', 27:229-235.

* J. Minker (1982). On indefinite databases and the closed world assumption. In ''Proceedings of the Sixth International Conference on Automated Deduction(CADE'82）'', pages 292-308.

* A. Rajasekar, J. Lobo, and J. Minker (1989). Weak generalized closed world assumption. ''Journal of Automated Reasoning'', 5:293-307.

* R. Reiter (1978). On closed world data bases. In H. Gallaire and J. Minker, editors, ''Logic and Data Bases'', pages 119-140. Plenum Publ.\ Co., New York.
{{reflist}}

==外部链接==

* https://web.archive.org/web/20051220205009/http://cs.wwc.edu/~aabyan/Logic/CWA.html
* https://web.archive.org/web/20090624113015/http://www.betaversion.org/~stefano/linotype/news/91/
* http://esw.w3.org/topic/ClosedWorldAssumptions {{Wayback|url=http://esw.w3.org/topic/ClosedWorldAssumptions |date=20070607164326 }}

[[Category:计算机逻辑]]
[[Category:数据库]]