1998 Fiscal Year Annual Research Report
順序ソート型理論に基づく知識表現と推論に関する研究
| Project/Area Number |
10878055
|
|---|
| Research Institution | Kyushu Institute of Technology |
|---|
Principal Investigator |
原尾 政輝 九州工業大学, 情報工学部, 教授 (00006272)
|
|---|
| Keywords | 型理論 / ラムダ計算 / 知識表現 / 推論処理 / 順序ソート / 2階単一化 / 継承 / 述語論理 |
|---|
| Research Abstract |
型理論に順序構造を導入した順序ソート型理論によって,モジュール表現や継承機構を備えた論理型言語と推論処理の実現が期待できる.本年度の研究ではこの観点から,理論的な性質を明らかにする問題に焦点を絞って研究を行った.まず単純型付きラムダ計算体系を基に,順序ソート型理論の定式化を行った.従来の型推論では幾つかの非整合的な性質があることから,新しく制限関数の概念に基づいた部分型関係を導入し,ラムダ計算の演算規則や代入法則などの基本的資質を明らかにした.さらに,変数変換によって継承機構を整合的に実現するラムダ計算体系を定義した.ラムダ計算体系は,論理型を導入することによって自然に高階論理言語を定義可能であり,人工知能で有用な推論機構を明快に与えることが出来る.型を概念に部分型関係を概念間の順序構造と見なす観点から階層的知識表現としての性質を考察した.また,部分型による型推論規則を与え,型継承に基づく推論処理と証明論としての性質を明らかにした.推論処理を自動化する上で高階単一化,高階一般化が重要な問題であるが,順序ソートの場合には確立されていない。一般の高階単一化は計算不能であり実用の観点からもあまりにも範囲が広すぎる.そのため,本研究では2階論理式のマッチングに焦点を絞り効率的アルゴリズムの設計の観点からの研究を行った.順序を考慮しない場合は多項式計算量のヒューリスティックを導入したアルゴリズムが得られた.更に順序構造を導入した2階述語マッチングへの拡張を行っている状況である.型順序関係を用いた論理体系についてそのクリプケ可能世界意味論を与え,一つの可能世界を知識モジュールと見なすことによって,モジュール構造をもった論理プログラム理論としての意味付けが可能である.まだ,順序ソート型理論と論理体系,継承や型変換の機能を備えたモジュール理論との完全な融合は出来ていないが,人工知能基礎論における知識表現と推論に新しい発展をもたらす可能性を秘めており,今後も研究を推進する計画である.
|
-
[Publications] 原尾政輝: "順序ソート型付ラムダ計算における簡約と単一化" 数理解析研究所講究録. 1041. 219-226 (1998)
-
[Publications] 山田,平田,原尾: "決定可能な高階単一化問題に関する研究" 数理解析研究所講究録. 1041. 227-234 (1998)
-
[Publications] J.Lu,M.Hagiya,M.Harao: "Higher Order Generalization" Lecture Notes in AI. No.1489. 368-381 (1998)
-
[Publications] 山田,平田,原尾: "二階論理スキーマにおけるマッチングについて" 情報基礎理論ワークショップ予稿集. 7-13 (1998)
-
[Publications] 平田,山田,原尾: "Tractable and Intractable Second-Order Matching Problems" 情報基礎理論ワークショップ予稿集. 1-6 (1998)
-
[Publications] 山田,平田,原尾: "二階論理スキーマにおけるマッチングと計算量" 電子情報通信学会研究会. COMP98-56. 41-48 (1998)
