ロジカルフレームワーク理論に基づく推論原理とその発見的推論システムへの応用

1996 Fiscal Year Annual Research Report

• Project/Area Number: 07680405
• Research Institution: KYUSHU INSTITUTE OF TECHNOLOGY
• Principal Investigator: 原尾 政輝 九州工業大学, 情報工学部, 教授 (00006272)
• Keywords: 論理 / 型理論 / ロジカルフレームワーク / 知的推論原理 / 仮説推論 / 類推 / 発見的推論 / 知能言語

Research Abstract

平成7年度は、知的推論システムのための発見的推論原理を確立する観点から、ロジカルフレームワーク理論に基づく推論原理および知能言語に関する理論的研究を中心に行ない、平成8年度は、発見的推論システムの開発研究を中心に、研究計画に沿って,(1)ロジカルフレームワーク理論に基づく知能処理言語に関する研究,(2)ロジカルフレームワーク理論に基づく証明の自動生成に関する研究,(3)類推に基づく証明発見システムの開発研究,の課題を中心に研究を行なった。各研究課題に対する研究成果は概略以下の通りである。
(1)の課題に関する研究概要:ロジカルフレームワーク理論に基づいて、種々のデータや知識の表現法、および処理の効率化のための継承機構の理論的性質を考察した。また、その結果に基づいてより柔軟な知識表現が可能で、継承処理機能を持つ知能言語を設計しワークステーション上で実装した。
(2)の課題に関する研究概要:型理論の特長である型推論機構と論理の証明系であるシークエント計算との融合を図り、高階の導出証明法や単一化理論、などについて考察した。さらに、型理論における式即是型原理と論理における証明との関係を文法として定式化する手法を提案し、その推論への応用についても興味ある結果を得た。
(3)の課題に関する研究概要:人間に近い形で推論し問題の解を発見するシステムを一般的な証明系であるシークエント計算の上で類推証明システムとしてモデル化し、一般定理証明用言語であるIsabelleを用いてSUNワークステーション上に実現した。
この研究を通して、ロジカルフレームワーク理論が、人工知能の推論原理や知能処理言語に対して有用であることを検証することができた。また、得られた知見を基にこの方法論を発展させていく予定である。

Research Products

• [Publications] 原尾政輝: "高階順序ソ-ト型理論における部分型と継承の意味論" 電子情報通信学会技術報告. COMP95-28. 19-28 (1995)
• [Publications] 原尾政輝: "型理論に基づく知識表現言語の実現" 人工知能学会全国大会論文集. 9. 13-16 (1995)
• [Publications] 足達、原尾: "順序付型理論による継承の定式化" 電気関係学会九州支部大会論文集. 1995年度. 1331-1331 (1995)
• [Publications] 山田,平田,原尾: "型付きラムダ計算における証明文法" 電子情報通信学会技術報告. COMP95-58. 11-20 (1995)