論理学における形式化
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2019/08/30 17:09 UTC 版)
論理学における閉世界仮説の最初の形式化は、知識ベースに含まれないリテラル群について、その否定を知識ベースに加えることとされた。この場合、知識ベースがホーン節で表されるなら一貫性が保たれるが、そうでない場合は必ずしも一貫性は保たれない。例えば、次のような知識ベース { E n g l i s h ( F r e d ) ∨ I r i s h ( F r e d ) } {\displaystyle \{English(Fred)\vee Irish(Fred)\}} では、 E n g l i s h ( F r e d ) {\displaystyle English(Fred)} も I r i s h ( F r e d ) {\displaystyle Irish(Fred)} も含まれていない（フレッドはイギリス人かアイルランド人であり、どちらであるかは知識として確定していない）。 ここで、それらの否定を知識ベースに加えると次のようになる。 { E n g l i s h ( F r e d ) ∨ I r i s h ( F r e d ) , ¬ E n g l i s h ( F r e d ) , ¬ I r i s h ( F r e d ) } {\displaystyle \{English(Fred)\vee Irish(Fred),\neg English(Fred),\neg Irish(Fred)\}} これでは一貫性がない（フレッドはイギリス人でもアイルランド人でもないことになり、元の知識と矛盾する）。換言すれば、閉世界仮説を形式化すると一貫性のある知識ベースが一貫性を失う場合がある。閉世界仮説を導入して一貫性が失われないのは、知識ベース K {\displaystyle K} の全てのエルブランモデルの交差と K {\displaystyle K} のモデルとが等価である場合だけである。命題論理の場合、この条件は K {\displaystyle K} が単一の最小のモデルしか持たないことと等価であり、モデルが最小とは真である変項の部分集合を持つ他のモデルが存在しないことを意味する。 このような問題を起こさない別の形式化が提案されてきた。以下では、知識ベース K {\displaystyle K} は命題論理的であると仮定する。どのような場合も、閉世界仮説の形式化では K {\displaystyle K} において否定してもよい論理式の否定形を K {\displaystyle K} に追加することを基本とする。つまり、それらの論理式は偽であると仮定される。換言すれば、命題論理式 K {\displaystyle K} に閉世界仮説を適用すると次のような論理式が生成される。 K ∧ { ¬ f | f ∈ F } {\displaystyle K\wedge \{\neg f~|~f\in F\}} . 集合 F {\displaystyle F} は K {\displaystyle K} において否定してもよい論理式の集合である。この F {\displaystyle F} の定義を変えることで閉世界仮説の形式化が変わってくる。以下に f {\displaystyle f} の様々な定義によって得られる（閉世界仮説の）形式化を列挙する。 CWA（閉世界仮説） f {\displaystyle f} は K {\displaystyle K} に存在しない肯定形のリテラルである。 GCWA （一般化CWA） f {\displaystyle f} は肯定形のリテラルであり、全ての肯定形の節 c {\displaystyle c} は K ⊭ c {\displaystyle K\not \models c} であり、 T ⊭ c ∨ f {\displaystyle T\not \models c\vee f} が成り立つ。 EGCWA （拡張GCWA） GCWA とほぼ同様だが、 f {\displaystyle f} は肯定形のリテラルの論理積である。 CCWA （careful CWA） GCWA とほぼ同様だが、肯定節として所定の集合に含まれる肯定リテラルと別の集合にあるリテラルから構成されるものだけに限定される。 ECWA （拡張CWA） CCWA とほぼ同様だが、 f {\displaystyle f} は所定の集合に含まれないリテラルからなる任意の論理式である。 ECWA とサーカムスクリプションの形式化は命題論理においては等価である。ある論理式が閉世界仮説の下で別の論理式に含まれているかどうかを確かめることの複雑性は、通常は論理式の多項式階層の第二レベルであり、ホーン節についてはPとcoNPの間にある。本来の閉世界仮説を導入することで一貫性を失うかどうかの判定はNP預言機械を最大でも対数回呼び出す必要があるが、この問題の正確な複雑性は未知である。
※この「論理学における形式化」の解説は、「閉世界仮説」の解説の一部です。
「論理学における形式化」を含む「閉世界仮説」の記事については、「閉世界仮説」の概要を参照ください。
- 論理学における形式化のページへのリンク
