封閉世界假定

封閉世界假定是當前不是已知的事物都為假的假定。這個名字也稱呼Ray Reiter對這個假定的邏輯形式化。與封閉世界假定相對立的使用開放世界假定，宣稱知識的缺乏不蘊涵虛假。

否定為失敗與封閉世界假定有關，因為它總體上相信不能被證明為真的所有命題都是假的。

封閉世界假定經常暗含在數據庫中，因為所有沒有明確的包換在表中記錄都暗含的假定表示這是假（而不是未知）這個事實。例如，如果數據庫包含下列表，報告寫作給定文章的人的，關於沒有編輯形式邏輯的文章的人的查詢，經常被預期返回「Sarah Johnson」。

編輯
編輯者	文章
John Doe	形式邏輯
Joshua A. Norton	形式邏輯
Sarah Johnson	空間數據庫導論
Charles Ponzi	形式邏輯
Emma Lee-Choon	形式邏輯

這個結果服從表中不包含Sarah在第一個位置而「形式邏輯」在第二個位置的行的事實。這個論證暗含的是基於表中缺乏「Sarah|形式邏輯」這樣的行蘊涵Sarah沒有編輯關於形式邏輯的文章的假定。所以，這個查詢的結果基於的是封閉世界假定，與之相對，在開放世界假定中，沒有明確的陳述的事物是未知的而不是假的。在開放世界假定中，Sarah編輯這個文章是未知的；在封閉世界假說中，她沒有編輯這個文章是已知的。

邏輯形式化

封閉世界假定首要邏輯形式化在於向知識庫增加當前不被它所蘊涵的文字。如果知識庫是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.

1. Carlo Zaniolo. Advanced Database Systems. Morgan Kaufmann Publishers. 1997: 183. ISBN 1-55860-443-X.

外部連結

• 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 （頁面存檔備份，存於互聯網檔案館）