| 研究課題/領域番号 |
26540110
|
|---|
| 研究機関 | 北海道大学 |
|---|
研究代表者 |
赤間 清 北海道大学, -, 名誉教授 (50126265)
|
|---|
| 研究期間 (年度) |
2014-04-01 – 2017-03-31
|
| キーワード | モデル・インターセクション問題 / 求解問題 / 証明問題 / 等価変換 / スコーレム化 / 意味保存 / 論理構造 / 節 |
|---|
| 研究実績の概要 |
モデル・インターセクション問題という問題のクラスを導入した。これは、求解問題や証明問題の最も一般的なクラスを包含する問題クラスである。すべての求解問題や証明問題は、モデル・インターセクション問題に帰着でき、モデル・インターセクション問題の解法を用いて解くことができる。このモデル・インターセクション問題は、特殊化システムをパラメータとする論理構造に基づく問題クラスであり、特殊化システムを具体的に指定することにより、いろいろなデータ構造を持つ領域に適用できる。
この一般クラスに対して等価変換による解法を定式化し、解の正当性を証明した。この解法は、レゾリューション法などより一段高い位置にある「一般スキーマ」であり、多様な解法を生成できる。証明問題に対するレゾリューション法やPrologの求解問題に対するＳＬＤレゾリューション法などを生み出すばかりか、新しい解法を生み出すことができる。これは、等価変換に基づく解法が問題構造からみて本質的な解法であることを示唆している。
既存のスコーレム化と、我々の提案する「意味保存スコーレム化」とを比較して、関数変数除去という変換を提案し、それが等価変換であることを示した。従来のスコーレム化は、「意味保存スコーレム化」と関数変数除去変換の合成とみなすことができる。関数変数除去変換の適用範囲の狭さにより、既存のスコーレム化の限界を指摘し、「意味保存スコーレム化」を基盤とする解法の汎用性、優秀性を明確に示した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
モデル・インターセクション問題という問題のクラスを新たに導入した。またこの一般クラスに対して等価変換による解法を定式化し、解の正当性を証明した。この解法は、レゾリューション法などより一段高い位置にある「一般スキーマ」であり、多様な解法を生成できる。既存の方法を説明することもできるし、新しい解法を生み出すこともできる。また、既存のスコーレム化の限界を指摘し、「意味保存スコーレム化」を基盤とする解法の汎用性、優秀性を明確に示した。これは今年度の目標を達成している。また多様な論理的問題の研究の新しい強力な基盤を提供することが期待される。
|
| 今後の研究の推進方策 |
モデル・インターセクション問題は、特殊化システムをパラメータとする論理構造に基づく問題クラスであり、特殊化システムを具体的に指定することにより、いろいろなデータ構造を持つ領域に適用できる。次年度はこの理論を、関数変数を含む理論に拡張する。これによって、「意味保存スコーレム化」が切り開いた新しい世界のすべてを受け止める理論を構築できることになる。モデル・インターセクション問題を解く実験システムの増強や新しい問題を解く実験を進め、より大きな問題を高速に解く技術の開発も検討する。
|
| 次年度使用額が生じた理由 |
1月2月に予定していた研究打ち合わせ出張の予定を変更し、システム構築と実験に切り替えたことにより、次年度使用額が生じた。
|
| 次年度使用額の使用計画 |
今年度にできなかった分の研究打ち合わせ出張を次年度に行う。
|
