| 研究概要 |
平成5年度は平成4年度結果を踏まえて次の具体的課題を設定して研究を進めてきた.
(1)型理論に基づく知識表現と推論機構の研究,(2)高階プログラム言語の設計と処理系の作成,(3)高階抽象化に基づく類推システムの実現.
まず(1)の課題に対しては,ロジカルフレームワーク型理論に基づく知識の表現と理論的性質を明らかにした.特に,型=命題=概念の考え方を新たに導入して,概念階層や知識構造に新しい意味を与えた.そして,その性質を用いて継承が実現でき,一般化,単一化がより精密に実現可能であることを示した.
次の(2)の課題については,ロジカルフレームワーク型理論に基づく課題(1)で得られた高階プログラミング言語を設計し,言語MLを用いて実験システムを作成した.特徴としては,その処理系は型推論規則に基づいており,高階の知識表現や部分型による継承などの処理が可能な事である.
(3)の課題については,対象を一般的な証明問題であるLK定理証明システムを採り,これを高階抽象化に基づく類推として定式化し,実装した.システムの基本機能としては,問題の類似性を検出しスキーマ(2階の論理式)として一般化しスキーマベースを構成する過程,与えられた問題に対して適用可能なスキーマを検索し証明情報を計算する過程,証明情報から具体的証明を作り出す過程,からなる.現在,40程度のスキーマよりなるシステムとなっており,大学の初級程度の証明能力を備えている.
以上のように,型理論に基づく新しい手法で有用な知能ソフトウェア言語が実現可能な事を示すことができた.
|
