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

1995 Fiscal Year Annual Research Report

• Project/Area Number: 07680405
• Research Category: Grant-in-Aid for General Scientific Research (C)
• Research Institution: Kyushu Institute of Technology
• Principal Investigator: 原尾 政輝 九州工業大学, 情報工学部, 教授 (00006272)
• Keywords: 論理 / 型理論 / ロジカルフレームワーク / 知的推論原理 / 仮説推論 / 類推 / 発見的推論 / 知能言語

Research Abstract

本年度は、知的推論システムのための発見的推論原理を確立する観点から、研究計画に沿って以下の課題を中心に研究を行なった。
(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] 原尾政輝: "カテゴリー理論に基づくプログラミング言語の実現" 電気関係学会九州支部大会論文集. 1995年度. 1330-1330 (1995)
• [Publications] 原尾政輝: "型付きラムダ計算における証明文法" 電子情報通信学会技術報告. COMP95. 11-20 (1995)