封闭世界假定

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

${\displaystyle \{English(Fred)\vee Irish(Fred)\}}$ 

不蕴涵${\displaystyle English(Fred)}$ 也不蕴涵${\displaystyle Irish(Fred)}$ 。

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

${\displaystyle \{English(Fred)\vee Irish(Fred),\neg English(Fred),\neg Irish(Fred)\}}$ 

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

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

${\displaystyle K\wedge \{\neg f~|~f\in F\}}$ 。

${\displaystyle K}$ 的自由否定的公式集合${\displaystyle F}$ 可以用不同方式定义，这导致封闭世界假定的不同的形式化。下面是在各种形式化中是自由否定的${\displaystyle f}$ 的定义。

CWA（封闭世界假定）

${\displaystyle f}$ 是不被${\displaystyle K}$ 蕴涵的肯定文字；

GCWA（普遍CWA）

${\displaystyle f}$ 是肯定命题，使得对于${\displaystyle K\not \models c}$ 的所有肯定子句${\displaystyle c}$ ，${\displaystyle T\not \models c\vee f}$ 成立；

EGCWA（扩展GCWA）

同上，但${\displaystyle f}$ 是肯定文字的合取；

CCWA（仔细CWA）

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

ECWA（扩展CWA）

类似于CCWA，但是${\displaystyle f}$ 是不包含来自给定集合的文字的任意公式。

ECWA和界限的公式化在命题理论上是一致的。查询答复的复杂性（在封闭世界假定下检查一个公式是否被另一个公式所蕴涵）对于一般公式集典型的是在多项式层次中第二级中的，并且对于Horn公式范围是从P到coNP。检查最初的封闭世界假定是否介入矛盾，要求对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）)为真，即张师傅不给自己理发。于是得出矛盾结论。

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

• 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 ${\displaystyle \Pi _{2}^{p}}$ -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.

• 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 （页面存档备份，存于互联网档案馆）