マルチエージェント環境のための様相論理に対する推論システムの研究

マルチエージェント環境のための様相論理に対する推論システムの研究について,今年度は以下の3つのテーマについて研究を行った.1.マルチエージェントシステムに対する知識と時間の様相論理体系の確立(1)各エージェントが「命題pがある時点tで成り立つことを知っている」というような知識と時間に関する表現が可能な様相論理体系MAKTを提案した.(2)論理体系MAKTの意味論は可能世界モデル意味論によって定義される.また,MAKTの式に対する推論は,MAKTの式をそれと等価な(不等号につき)一階述語論理の式に変換されて,その一階述語論理式の充足可能性を調べることによって行われる.(3)以上の結果より,論理体系MAKTに対する効率的な推論方法は,高速な一階述語用の定理証明器を開発することに帰着されるという知見を得た.2.一階述語定理証明器SATCHMOREの効率化一階述語用の定理証明器の一つにSATCHMOREがあるが,本研究においては,それに更に改良を行い効率化を図った.すなわち,SATCHMOREで用いられている関連性に加えて,“利用可能性"という新しい条件を付け加えて,定理証明における探索空間の減少を図った.3.融合型知識ベースに対する推論方式の検討複数の知識ベース(エージェント)が与えられたとき,それらの知識を融合して推論を行う融合型知識ベース(amalgamated knowledge databases)に対する推論方法について検討を行った.

マルチエージェント環境のための様相論理に対する推論システムの研究について,今年度は以下の3つのテーマについて研究を行った.1.マルチエージェントシステムに対する知識と時間の様相論理体系の確立(1)各エージェントが「命題pがある時点tで成り立つことを知っている」というような知識と時間に関する表現が可能な様相論理体系MAKTを提案した.(2)論理体系MAKTの意味論は可能世界モデル意味論によって定義される.また,MAKTの式に対する推論は,MAKTの式をそれと等価な(不等号につき)一階述語論理の式に変換されて,その一階述語論理式の充足可能性を調べることによって行われる.(3)以上の結果より,論理体系MAKTに対する効率的な推論方法は,高速な一階述語用の定理証明器を開発することに帰着されるという知見を得た.2.一階述語定理証明器SATCHMOREの効率化一階述語用の定理証明器の一つにSATCHMOREがあるが,本研究においては,それに更に改良を行い効率化を図った.すなわち,SATCHMOREで用いられている関連性に加えて,“利用可能性"という新しい条件を付け加えて,定理証明における探索空間の減少を図った.3.融合型知識ベースに対する推論方式の検討複数の知識ベース(エージェント)が与えられたとき,それらの知識を融合して推論を行う融合型知識ベース(amalgamated knowledge databases)に対する推論方法について検討を行った.