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

1996 Fiscal Year Annual Research Report

• Project/Area Number: 08680397
• Research Category: Grant-in-Aid for Scientific Research (C)
• Research Institution: Nagoya Institute of Technology
• Principal Investigator: 世木 博久 名古屋工業大学, 工学部・知能情報システム学科, 助教授 (90242908)
• Keywords: マルチエージェント / 様相論理 / 定理の自動証明

Research Abstract

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

Research Products

• [Publications] Lifeng He: "Implementing an Automated Reasoning System for Multi-Agent Knowledge and Time" Proc.PRICAI'96 Workshop on Distributed Artificial Intelligence. 44-57 (1996)
• [Publications] Lifeng He: "A Nulti-Agent Cooperative Reasoning System for Analganoted Knouledge Bases" Proc.PRICAI'96 Workshop on Distributed Aritificial Intelligence. 88-101 (1996)
• [Publications] 何立風: "定理証明器SATCHMOREの効率化に関する一手法" 情報処理学会論文誌. (探録決定).