| 研究概要 |
アブダクションによるルール生成を,モデルに基づくアブダクションと型理論におけるアブダクションという二つの側面から研究を進めた.
モデルに基づくアブタクションでは,特に例からの論理プログラムの学習である帰納論理プログラミングとの関連から研究を進めた.モデルに基づくアブダクションは,属性値データからの学習や解釈からの帰納論理プログラミングと密接な関係があり,これらの枠組みでは,一般に関数記号を考えない.一方,平坦化とは,関数記号を含む論理プログラムを関数記号無し論理プログラムに変換する技法である.よって平坦化は,帰納論理プログラミングからモデルに基づくアブダクションヘの橋渡しとなることが期待できる.本研究では,平坦化が,帰納論理プログラミングの重要な意味である包摂関係・含意関係のを保存するか否かについて厳密な解を得ることができた.
型理論におけるアブダクションでは,最も基本的な技法になると思われる,単一化問題の計算量について研究を進めた.一階項に関数変数を許した項を二階項といい,二階項の単一化問題を二階単一化問題,二階項と変数を含まない一階項の単一化問題を二階マッチング問題という.一般に一階単一化問題は多項式時間で解けるが,二階単一化問題は決定不能であり,二階マッチング問題もNP完全である.本研究では,二階マッチング問題の計算量を細密に解析した.そして,関数変数の引数の数,関数変数の出現数,関数定数の有無,個体変数の有無,関数変数の引数に関数変数を含むか否か,という制限を加えることにより,NP完全となる二階マッチング問題と多項式時間で解ける二階マッチング問題を明確に特徴づけることに成功した.さらに,多項式時間で解ける二階マッチング問題を,スキーマ誘導証明におけるスキーママッチングに適用した.
|
