自己認識論理

自己認識論理（英: Autoepistemic logic）とは、知識に関する知識を表現したり推論したりするために定式化された形式論理である。命題論理は事実しか表現できないが、自己認識論理は知識やある事実に関する知識がないことを表現できる。

安定モデル意味論は、自己認識論理を単純化したものと見ることができる。安定モデル意味論は失敗による否定のある論理プログラミングの意味論として使われている。

統語論

自己認識論理の統語論は、命題論理に知識を表す様相作用素 $◻$ を追加したものである。$F$ を論理式としたとき $◻F$ は $F$ が既知であることを意味する。したがって $◻\mathrm{\neg }F$ は $\mathrm{\neg }F$ が既知であることを意味し、$\mathrm{\neg }◻F$ は $F$ を知らないことを意味する。

この統語論により、事実に関する知識に基づく推論が可能となる。例えば、$\mathrm{\neg }◻F\to \mathrm{\neg }F$ は、$F$ が真であることが未知ならば、それを偽とみなすことを意味する。これは失敗による否定に他ならない。

意味論

自己認識論理の意味論は推論の展開に基づくもので、命題論理のそれと類似した役割を持つ。命題論理モデルでは個々の原子項の真偽を指定するが、この拡張においては個々の論理式 $◻F$ の真偽を指定する。特に自己認識論理式 T の展開は、$T$ に含まれる全ての部分論理式 $◻F$ についてこの指定をする。$◻$ を含む全ての部分論理式は真偽のどちらかなので、この指定は $T$ を命題論理式として扱うことを可能にする。特にこの条件において、$T$ が $F$ を内含するかどうかは命題論理の規則でチェック可能である。初期の前提が展開であるため、部分論理式 $F$ が内含されるのは、$◻F$ が初期の前提として真とされた場合のみである。

例えば、論理式 $T=◻x\to x$ において、ボックス部分論理式は $◻x$ のひとつだけである。従って、考慮すべき展開は真と偽の2種類だけである。実際には、以下のようになる。

$◻x$ を偽と仮定した場合

$◻x\to x$ は $\mathrm{\neg }◻x\vee x$ と等価であり、$\mathrm{\neg }◻x$ は真とされているので、$T$ は（仮定が成り立つ限り）恒に真である。従って $x$ は内含されない。$◻x$ が偽ということは $x$ は既知ではないので、この結論が暗に裏付けられる。従って、$◻x$ が偽であるという前提は展開である。

$◻x$ を真と仮定した場合

$T$ は $x$ を内含する。従って $◻x$ が真であるという当初の前提に含まれる暗黙の前提、すなわち $x$ が真であると知られていることは充足している。結果として、これはもう1つの展開である。

従って論理式 $T$ は2つの展開を持ち、その1つでは $x$ は未知であり、もう1つでは $x$ は既知である。後者の場合、$◻x$ が真であるという初期前提が $x$ が真であることの唯一の裏づけであるため、直観的でない。言い換えれば、これは自立した仮定である。このような自立した信念を扱う論理を not strongly grounded と言い、そうでない論理を strongly grounded と言う。strongly grounded な自己認識論理も存在する。

関連項目

• 非単調論理
• 様相論理学

参考文献

• G. Gottlob (1995). Translating default logic into standard autoepistemic logic. Journal of the ACM, 42:711-740.
• T. Janhunen (1998). On the intertranslatability of autoepistemic, default and priority logics. In Proceedings of the Sixth European Workshop on Logics in Artificial Intelligence (JELIA'98), pages 216-232.
• W. Marek and M. Truszczynski (1991). Autoepistemic logic. Journal of the ACM, 38(3):588-619.
• R. C. Moore (1985). Semantical considerations on nonmonotonic logic. Artificial Intelligence, 25:75-94.
• I. Niemelä (1988). Decision procedure for autoepistemic logic. In Proceedings of the Ninth International Conference on Automated Deduction (CADE'88), volume 310 of Lecture Notes in Computer Science, pages 675-684. Springer.