順序ソート型理論に基づく知識表現と推論に関する研究

型間に順序構造を導入した順序ソート型理論はフレーム的知識表現構造と継承機構を形式化するために有用であることが指摘され,新しい言語や知識処理モデルが研究されている。本研究は,順序ソート型理論をベースに人工知能のためのフレーム構造知識表現と継承機構を備えた推論処理を形式化し実現する観点から考察を行った。まず,単純型付きラムダ計算体系を基に順序ソート型理論の定式化を行い,従来の非整合的な問題点をなくすために,新しく制限関数の概念に基づいた部分型関係を導入し,ラムダ計算の演算規則や代入法則などの基本的性質を明らかにすると共に,変数変換によって継承機構を整合的に実現するラムダ計算体系を定義した。また,型を概念に部分型関係を概念間の順序構造と見なす観点から階層的知識表現としての性質を考察し,部分型による型推論規則を与え,型継承に基づく推論処理ととしての性質を明らかにした.次いで,推論処理を自動化する上で高階単一化が重要な問題であるが,順序ソートの場合には確立されていない。一般の高階単一化は計算不能であり実用の観点からもあまりにも範囲が広すぎる.そのため,本研究では2階論理式のマッチングに焦点を絞り効率的アルゴリズムの設計の観点からの研究を行った.順序を考慮しない場合は多項式計算量のヒューリスティックを導入したアルゴリズムが得られた.更に順序構造を導入した2階述語マッチングへの拡張を行った。また,高階一般化についても多層型の概念を用いて,知識の抽象化や一般化の観点から一つの手法を与えた。これらの結果を用いて,順継承や型変換の機能を備えたモジュール理論などの考察も行い,人工知能基礎論における知識表現と推論に新しい理論展開を行った。

型間に順序構造を導入した順序ソート型理論はフレーム的知識表現構造と継承機構を形式化するために有用であることが指摘され,新しい言語や知識処理モデルが研究されている。本研究は,順序ソート型理論をベースに人工知能のためのフレーム構造知識表現と継承機構を備えた推論処理を形式化し実現する観点から考察を行った。まず,単純型付きラムダ計算体系を基に順序ソート型理論の定式化を行い,従来の非整合的な問題点をなくすために,新しく制限関数の概念に基づいた部分型関係を導入し,ラムダ計算の演算規則や代入法則などの基本的性質を明らかにすると共に,変数変換によって継承機構を整合的に実現するラムダ計算体系を定義した。また,型を概念に部分型関係を概念間の順序構造と見なす観点から階層的知識表現としての性質を考察し,部分型による型推論規則を与え,型継承に基づく推論処理ととしての性質を明らかにした.次いで,推論処理を自動化する上で高階単一化が重要な問題であるが,順序ソートの場合には確立されていない。一般の高階単一化は計算不能であり実用の観点からもあまりにも範囲が広すぎる.そのため,本研究では2階論理式のマッチングに焦点を絞り効率的アルゴリズムの設計の観点からの研究を行った.順序を考慮しない場合は多項式計算量のヒューリスティックを導入したアルゴリズムが得られた.更に順序構造を導入した2階述語マッチングへの拡張を行った。また,高階一般化についても多層型の概念を用いて,知識の抽象化や一般化の観点から一つの手法を与えた。これらの結果を用いて,順継承や型変換の機能を備えたモジュール理論などの考察も行い,人工知能基礎論における知識表現と推論に新しい理論展開を行った。