閉世界仮説
閉世界仮説（へいせかいかせつ、英: Closed world assumption）は、現時点で真であると判明していないことは偽であると仮定することを意味する。論理学では、Raymond Reither が閉世界仮説を形式化した。閉世界仮説の逆を開世界仮説（Open world assumption）と呼び、知識の欠如を偽とは見なさない。
Contents
概要
失敗による否定（Nagation as failure）は閉世界仮説と関連しており、真であると証明されなかった述語は偽であると見なされる。
ナレッジマネジメントでは、閉世界仮説が少なくとも2つの状況で使われる。第一に、知識ベースが完成した時点で、そこに含まれない知識は偽であるとされる。例えば、企業の従業員のデータベースが完全であれば、そこに記録されていない人は従業員ではない。第二に、知識ベースが不完全であるときでも、そこにない知識は偽であるとして回答することが最善の場合である。例えば、以下のような編集者と記事名の表がデータベースにあったとき、"Formal Logic" の編集に関わっていない編集者というクエリに対しては “Sarah Johnson” と答えることが期待される。
| Edit | |
|---|---|
| Editor | Article |
| John Doe | Formal Logic |
| Joshua A. Norton | Formal Logic |
| Sarah Johnson | Introduction to Spatial Databases |
| Charles Ponzi | Formal Logic |
| Emma Lee-Choon | Formal Logic |
閉世界仮説では、この表が完全である（全ての編集者と記事の対応が格納されている）と仮定され、この表の中では Sarah Johnson だけが Formal Logic に関わっていない編集者とされている。もしここで開世界仮説を採用すれば、この表には全ての情報（編集者と記事の対応）が格納されていないと考えられ、答えが得られない。つまり、この表に載っていない編集者がどれだけいるか、Sarah Johnson が関わってこの表に載っていない記事がどれだけあるか分からないのである。
論理学における形式化
論理学における閉世界仮説の最初の形式化は、知識ベースに含まれないリテラル群について、その否定を知識ベースに加えることとされた。この場合、知識ベースがホーン節で表されるなら一貫性が保たれるが、そうでない場合は必ずしも一貫性は保たれない。例えば、次のような知識ベース
- [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] の全てのエルブランモデルの交差と [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]F[/math] は [math]K[/math] において否定してもよい論理式の集合である。この [math]F[/math] の定義を変えることで閉世界仮説の形式化が変わってくる。以下に [math]f[/math] の様々な定義によって得られる（閉世界仮説の）形式化を列挙する。
- CWA（閉世界仮説）
- [math]f[/math] は [math]K[/math] に存在しない肯定形のリテラルである。
- GCWA （一般化CWA）
- [math]f[/math] は肯定形のリテラルであり、全ての肯定形の節 [math]c[/math] は [math]K \not\models c[/math] であり、[math]T \not\models c \vee f[/math] が成り立つ。
- EGCWA （拡張GCWA）
- GCWA とほぼ同様だが、[math]f[/math] は肯定形のリテラルの論理積である。
- CCWA （careful CWA）
- GCWA とほぼ同様だが、肯定節として所定の集合に含まれる肯定リテラルと別の集合にあるリテラルから構成されるものだけに限定される。
- ECWA （拡張CWA）
- CCWA とほぼ同様だが、[math]f[/math] は所定の集合に含まれないリテラルからなる任意の論理式である。
ECWA とサーカムスクリプションの形式化は命題論理においては等価である。ある論理式が閉世界仮説の下で別の論理式に含まれているかどうかを確かめることの複雑性は、通常は論理式の多項式階層の第二レベルであり、ホーン節についてはPとcoNPの間にある。本来の閉世界仮説を導入することで一貫性を失うかどうかの判定はNP預言機械を最大でも対数回呼び出す必要があるが、この問題の正確な複雑性は未知である。
関連項目
参考文献
- 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.