1992 Fiscal Year Annual Research Report
| Project/Area Number |
04229217
|
|---|
| Research Institution | Kyushu Institute of Technology |
|---|
Principal Investigator |
原尾 政輝 九州工業大学, 情報工学部, 教授 (00006272)
|
|---|
| Keywords | 型理論 / 知識表現 / 概念階層 / 抽象化階層 / 一般化知識 / 高階単一化 / 類推 / 類推証明 |
|---|
| Research Abstract |
平成4年度は,次の具体的課題を設定して研究を進めた.(1)型の概念に基づく知識の類似性の定義.(2)類似性に基づく一般化知識の獲得,(3)類推システムの開発.
まず,(1)については,型理論に基づいて高階論理言語を設計し,その言語を用いて知識のデータ構造,型階層,知識のモジュール構造などの知識表現を定義した.そして,同じ型の要素は似ているとの観点から,概念階層,抽象化階層の考えを新たに導入して知識間の類似性を定義し,代数的(束論的)意味論を展開した.
次の(2)については,類似の知識集合を表す知識を一般化知識と呼び,概念階層や変数化(抽象化)による一般化知識の性質を性質を考察した.特に,対象とする知識を1階の論理式で表した場合の一般化知識を2階の論理式(これをスキーマとよぶ)として抽象化するための性質を明かにした.そして,高階単一化の手法を用いて,一般化知識を構成するアルゴリズムを設計した.特に,類推証明システムのための,類似証明を特性化するスキーマの導出法について幾つかの新しい結果を得た.
(3)の課題については,一般化知識を用いた類推システムを設計し,高階単一化に基づく手続きを与えた.またこの方式を,LK論理系の論理式の証明問題に応用し,類推に基づくLK類推証明システムを開発した.開発には言語Isabelleを用しており.スキーマ28個と誘導問題10個を持ち,初級の証明問題は解けるシステムとなっている.
|
-
[Publications] 中川 祥子,原尾 政輝: "類推によるLK定理証明" 電子情報処理学会,コンピュテーション研究会. COMP92-36. 63-70 (1992)
-
[Publications] M.Harao: "Analogical Reasoning For Natural Deduction Theorem Proving" Int.Workshop on Automated Reasoning(国際自動推論ワークショップ). Proceeding. 220-228 (1992)
-
[Publications] M.Harao: "LK Theorem proving By Analogy" 環太平洋人工知能国際会議(PRICAI'92). Proceeding. 714-720 (1992)
