型理論に基づく高階推論機構の形式化とその類推処理への応用

1993 Fiscal Year Annual Research Report

• Project/Area Number: 04650320
• Research Institution: Kyushu Institute of Technology
• Principal Investigator: 原尾 政輝 九州工業大学, 情報工学部, 教授 (44266272)
• Keywords: 型理論 / 知識表現 / 推論機構 / 知能ソフトウェア / 類推システム / 高階プログラム言語 / 定理証明 / 論理プログラム

Research Abstract

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

Research Products

• [Publications] 桜井,脇園,原尾: "抽象化に基づく類推" 情報処理. 34,No.5. 558-565 (1993)
• [Publications] 原尾: "Analogical Reasoning for LK Theorem Proving" Proc.of Tnter.Workshop on Automated Reasoning. North Hdland. 265-274 (1993)
• [Publications] 原尾,中川: "類似性に基づく一般化知識の獲得と推論" 人工知能学会全国大会(1993年度). 41-44 (1993)
• [Publications] 原尾,羽室: "高階の概念を用いた仮説推論" 1993年度電気関係九州支部大会. 688-688 (1993)
• [Publications] 原尾,村田: "LF理論に基づく論理型言語に関する一考察" 1993年度電気関係九州支部大会. 686-686 (1993)
• [Publications] 原尾: "型理論に基づく知識処理の定式化" シンポジウム-知識科学の最前線 論文集. 3-12 (1993)
• [Publications] 原尾 政輝: "人工知能アルゴリズム論" 近代科学社, 270 (1993)