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

Research Project

Project/Area Number	08680397
Research Category	Grant-in-Aid for Scientific Research (C)
Allocation Type	Single-year Grants
Section	一般
Research Field	Intelligent informatics
Research Institution	Nagoya Institute of Technology
Principal Investigator	世木博久名古屋工大, 工学部, 助教授 (90242908)
Project Period (FY)	1996 – 1998
Project Status	Completed (Fiscal Year 1997)
Budget Amount *help	¥1,900,000 (Direct Cost: ¥1,900,000) Fiscal Year 1997: ¥1,100,000 (Direct Cost: ¥1,100,000) Fiscal Year 1996: ¥800,000 (Direct Cost: ¥800,000)
Keywords	マルチエージェント / 様相論理 / 定理の自動証明
Research Abstract	マルチエージェント環境のための様相論理に対する推論システムの研究について,今年度は以下の3つのテーマについて研究を行った. 1.マルチエージェントシステムに対する知識と時間の様相論理体系の確立 (1)各エージェントが「命題pがある時点tで成り立つことを知っている」というような知識と時間に関する表現が可能な様相論理体系MAKTを提案した. (2)論理体系MAKTの意味論は可能世界モデル意味論によって定義される.また,MAKTの式に対する推論は,MAKTの式をそれと等価な(不等号につき)一階述語論理の式に変換されて,その一階述語論理式の充足可能性を調べることによって行われる. (3)以上の結果より,論理体系MAKTに対する効率的な推論方法は,高速な一階述語用の定理証明器を開発することに帰着されるという知見を得た. 2.一階述語定理証明器SATCHMOREの効率化一階述語用の定理証明器の一つにSATCHMOREがあるが,本研究においては,それに更に改良を行い効率化を図った.すなわち,SATCHMOREで用いられている関連性に加えて,“利用可能性"という新しい条件を付け加えて,定理証明における探索空間の減少を図った. 3.融合型知識ベースに対する推論方式の検討複数の知識ベース(エージェント)が与えられたとき,それらの知識を融合して推論を行う融合型知識ベース(amalgamated knowledge databases)に対する推論方法について検討を行った.