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

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

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