様相概念を用いる知識のモジュール化とその処理に関する研究

1992 年度 実績報告書

• 研究課題/領域番号: 04229204
• 研究機関: 北陸先端科学技術大学院大学
• 研究代表者: 米崎 直樹 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (00126286)
• キーワード: 概念定義 / 様相論理 / 時相論理 / 実現可能性 / プロセスモデル / 非標準論理 / 定理自動証明

研究概要

本研究では、様相を知識のモジュール化の基本とする概念記述のための論理体系と、概念モデルに関して研究を行ない以下の成果を得た。
昨年度導入され、untilより記述能力が高いことが証明された時相オペレータMore Thanを含む時想論理の、充足可能性判定問題が決定可能であることを証明すると同時に、具体的な決定手続きを与えた。また、Linear Logicは、並列処理に関する様々な性質を記述可能であるが、このような論理の証明を、計算プロセスと見做すことが出来れば都合が良い。そこで非節形式の導出法を考案し、その完全性と健全性を示した。その規則は、自然な並列計算のモデルと見做すことが可能である。一方、記述された概念が、どのような外界からの入力に関しても、常に反応する計算オブジェクトとして実現可能であるかを判定することは、実際に正しい仕様を得るためにも重要である。ここでは様々な実現可能性に関する性質を定義し、その概念階層について考察すると同時に、各性質の判定アルゴリズムを与えた。以上扱ってきた論理は、様々な様相論理体系として翻訳可能であるが、その証明体系を一般的に考察しておくことは、実際的証明系を構成する際に重要である。これまでに提案してきた、様相記号列の統一化を基にした一般的な様相論理証明体系に、モデルに於ける可能世界間の到達関係が推移的である場合に有効な統一化のスキーマを導入した。このような体系における証明には、同一の式が何度も使われる場合が多いが、ここではそのような証明の圧縮を、様相記号列の統一化における、自己代入という概念で表現可能であることを示した。またこのような考え方をuntilオペレータを含む時相論理体系に適用した場合について考察した。さらに、人間の活動を含めた仕事のプロセスを一般的に表現可能な、タスク、エージェントプロダクトを基本オブジェクトとするデータモデルについて提案を行なった。

研究成果

• [文献書誌] Noriaki Yoshiura,Naoki Yonezaki: "More expressive Temporal Logic for Specifications" The fifth International conference on Software Engeering and Knowledge Engeering. 28. (1993)
• [文献書誌] 川村 美代子,米崎 直樹: "Linear Logicの自動証明法" 第6回人工知能学会全国大会. 24. 95-98 (1992)
• [文献書誌] Ryousei Mori,Naoki Yonezaki: "Several Realizability Concepts in Reactive Objects" The Second European-Japanese Seminor on Information Modelling and Knowledge bases. (1992)
• [文献書誌] 端山 毅,米崎 直樹: "様相記号列統一化による様相論理定理証明器の健全性と完全性" コンピュータソフトウェア. Vol10,No.3. (1993)
• [文献書誌] 友石 正彦,米崎 直樹: "時相オペレータの統一化を用いる時相論理証明法" 日本ソフトウェア科学会第9回大会. 181-184 (1992)
• [文献書誌] Naoki Yonezaki,Tapani Kinnula,Motoshi Saeki,Jan Ljungberg: "A new model for software process Tasks-Agents-Products" The fifth International Conferece on Software Engeering and Knowledge Engeering. (1993)
• [文献書誌] Naoki Yonezaki: "Self-Substitution in Model Unification,Advances in Information Modelling and Knowledge Bases" IOS press, (1993)