人間は,新たな情報を得ることにより,
以前に得られた結論を覆すという種類の推論(非単調推論)を行うことがある.
そのような推論を形式化した論理に Moore (1985) の自己認識論理 (AutoEpistemic Logic, AEL) がある.
AELでは,理想的なエージェントが前提知識(自己認識理論)から推論して得られる知識集合を自己認識理論の拡張という.
また,AELを多重様相,多重理論に拡張した多エージェント系自己認識論理 (Multi-AutoEpistemic Logic, MAEL) が外山ら(1991)により提案された.
MAELを用いることにより,
属性継承や時間的因果関係に関する知識を表現することができる.
一方,Gelfond, Lifschitz (1988) はAELにおける自己認識理論の安定性の概念を利用して一般論理プログラムの安定モデル意味論を提案し,
一般論理プログラムの安定モデルがその一般論理プログラムを変換して得られる自己認識理論の拡張と対応していることを示した.
安定モデルの計算を効率的に行う種々の方法が提案されおり,
それらはAELの定理証明に利用できると考えられる.
本論文ではMAELにおける自己認識理論の安定性に注目し,
MAELと論理型プログラムの関係を解明する.
そのために,まず論理型プログラムのひとつであるMAELプログラムの構文を定義し,
その安定モデル意味論を定義した.
そして,MAELプログラムの安定モデルがそのMAELプログラムを変換して得られる多エージェント系自己認識理論の拡張と対応することを示した.
このことから,
MAELプログラムの安定モデルを計算することにより,
MAELの定理証明を行うことができる.