| 研究概要 |
高次の推論機構を実現するための重要な課題として類推機構や学習機能の実現がある.本研究では,型や高階の概念に基づく新しい手法によりこれらの問題に以下の課題を設定して取り組んだ.
(1)型理論に基づく知識構造と知識表現言語の設計.
(2)型および高階性の概念を用いた知識の類似性および一般化知識の獲得機構の定式化.
(3)類推システムの設計と具体的類推システムの実装.
その結果,本年度は次のような成果が得られた.
まず(1)の課題については,型に順序関係を導入した型順序をベースにして,型付lambda論理言語を定義し,この型順序によって知識間の階層構造や一般化知識および知識間の類似性が理論的に明確に定義できることを示した.また,高階性の概念を用いて類似な知識を特性化するスキーマの概念を導入し,一般化知識の表現の理論的枠組みを与えた.
(2)の課題に対しては,型の概念を下に知識間の類似性を定義し,知識を1階の型付きlambda式で,そして一般化知識を2階のlambda式であるスキーマで与えることによって,知識の一般的類似性を定式化した.知識の類似性の判定手続きを型順序単一化アルゴリズムを用いて与え,それを下に与えられた知識集合から逆単一化の手法を用いた一般化知識の獲得機構を定式化し実現した.
(3)の課題に対しては,最も定理証明システムとして一般的な枠組みを提供しているLK論理系の証明問題を対象として,類推による証明システムを設計し実現した.実現システムはSparcワークステーション上に言語Isabelleを用いて構築されており,約40のスキーマを持ち大学の初級程度の証明問題が対話形式で解けるものとなっている.このように,本研究では提案した研究課題に対して略満足できる成果を挙げることができ,今後もこれらの研究を発展させて行く計画である.
|
