様相論理とその実時間制御及び人工知能への応用
【研究分野】情報学
【研究キーワード】
様相論理 / 時制論理 / 形式的プログラム仕様 / 実時間制御システム / 知識表現 / 分散システム / 実行可能仕様言語 / 論理プログラミング / 実時間システム / プロセス制御 / 実行可能仕様 / 形式的仕様 / 分散オペレ-ティング・システム / ハイパ-テキスト / ソフトウェアの仕様 / 人工知能 / ユーザ・インターフェース
【研究成果の概要】
時制論理や区間論理を含む様相論理を応用して,プログラミングシステムの形式的記述や,人工知能における知識表現に有効な方法論や言語を構成する研究を試みた。言語RACCOは,時制様相論理を実行可能にした論理型言語で,モジュラ-構造を明示に表現する機能を有する。この言語を使用すれば,実用上の論議の対象となりうるほどに,十分に複雑な実時間プロセス制御システムの形式的記述が可能になる,処理系はCommon Lispで書かれ,プロトタイピングのためのグラフィック・シミレ-タも設計中である。一方,知識表現への応用としては,医療の分野を検討した。従来この分野では医療診断をエキスパ-ト・システムで自動化することをめざす研究が中心であったが,ここでは,従来のカルテを進化させた概念であるハイパ-・テキスト・システムの画面と対話しつつ,汎用及び個有知識ベ-スにアクセスしながら,医師が患者の検査,診断,治療を行うシステムを概念設計し,これを多世界多時間モデルに基づいて様相論理を拡張した論理系を用いて形式的記述を行った。加えて,当研究グル-プが,ここ数年間,外部団体などと共同に研究開発を行っている分散オペレ-ティング・システムであるToMの形式記述に様相論理を用いることも試みた。ToMではカ-ネル部分に最小限の並列性,分散性の機能を組み込み,この部分の正当性を確認することが,中心的な課題となるが,この目的のためには区間論理や時制論理による形式的記述と,それにもとづいて可能になる相互排除などの重要な性質の成立の確認が可能になることが示された。この研究の主な結果は,'90年にドイツのキ-ルで行われた国際学会の紹待講演で発表した。
【研究代表者】