|
本年度は、知的推論システムのための発見的推論原理を確立する観点から、研究計画に沿って以下の課題を中心に研究を行なった。
(1)ロジカルフレームワーク理論に基づく推論原理の研究。
(2)ロジカルフレームワーク理論に基づく知能言語の研究。
(3)発見的推論システムの開発研究。
各研究課題に対する研究成果は概略以下の通りである。
(1)の課題に関する研究概要:
型理論の特長である型推論機構と、論理の証明系であるシークエント計算との融合を図り、高階の導出証明法や単一化理論、などについて考察した。さらに、型理論における式即是型原理と論理における証明との関係を文法として定式化する手法を提案し、その推論への応用についても興味ある結果を得た。
(2)の課題に関する研究概要:
ロジカルフレームワーク理論を、型に順序に入れることによって拡張し、継承や推論処理に関する理論的性質を考察した。また、その結果に基づいてより柔軟な知識表現が可能で、継承処理機能を持つ知能言語を設計しワークステーション上で実装した。
(3)の課題に関する研究概要:
対象を一般的な証明系であるシークエント計算とし、人間に近い形で推論し証明するシステムを開発することを目標にし、システムの開発を行なった。特に、人間の発見的推論で基本的とされている、仮説および類似性を基に推論処理をする類推証明システムを定式化し一般定理証明用言語であるIsabelleを用いてSUNワークステーション上に実現した。この結果を基に、さらにより完成度の高いシステムへの拡張整備を計画している。
このように、初年度の目標である発見的推論原理についてはいくつかの基本的性質を明らかにし、今後の問題点や研究推進のための基本方針が定まり、次の研究へ向けての準備が整った状況である。
|
