| 研究概要 |
本研究の目的は,知的エージェントの数学的計算モデルを構築し,その論理的動作意味論に関する基礎理論を確立することである.具体的な研究実施項目と内容を以下に記す.
(1)エージェントのための計算モデルの構築
(2)エージェント計算の論理的意味論に関する数学的基礎理論の確立
(3)エージェント言語の開発(4)モデル検証システムの実装
本年度は,以下の項目に関して,以下の成果を得た.
(2b)モデル検証方法・システムの理論的構築
(2a)のベース論理に基づき,エージェントの論理的性質を検証するために,以下の3種類の検証方法・システムについて検討した.
演繹的手法:Gentzenのsequent計算風の合成性(compositionality)を有する証明システム.変換的手法:充足可能性に関して必要十分性を備えた論理式に変換し,充足可能であることとその論理式が真となることが等価であるような変換法.タブロー的手法:一般に,演繹システムを逆向き(トップダウン的)に用いるとタブロー的証明システムになるが,この小項目ではプロセスの構造によって定まる遷移関係に着目し,遷移関係に依存したシンボリックな証明システムを提案する.
(3)エージェント言語の開発(4)モデル検証システムの実装
(3)と(4)は,(1),(2)の成果に基づき,エージェント言語の開発と論理的意味をチェックするためのモデル検証システムを,初年度新設設備のスパークステーション上にjavaを用いて実装した.実装したシステムは,Web上に公開した.
|
