2015 Fiscal Year Research-status Report
「証明問題＋推論」から「求解問題＋等価変換」への大転換
| Project/Area Number |
26540110
|
|---|
| Research Institution | Hokkaido University |
|---|
Principal Investigator |
赤間 清 北海道大学, -, 名誉教授 (50126265)
|
|---|
| Project Period (FY) |
2014-04-01 – 2017-03-31
|
| Keywords | モデル・インターセクション問題 / 求解問題 / 証明問題 / 等価変換 / スコーレム化 / 意味保存 / 論理構造 / 節 |
|---|
| Outline of Annual Research Achievements |
モデル・インターセクション問題という問題のクラスを導入した。これは、求解問題や証明問題の最も一般的なクラスを包含する問題クラスである。すべての求解問題や証明問題は、モデル・インターセクション問題に帰着でき、モデル・インターセクション問題の解法を用いて解くことができる。このモデル・インターセクション問題は、特殊化システムをパラメータとする論理構造に基づく問題クラスであり、特殊化システムを具体的に指定することにより、いろいろなデータ構造を持つ領域に適用できる。
この一般クラスに対して等価変換による解法を定式化し、解の正当性を証明した。この解法は、レゾリューション法などより一段高い位置にある「一般スキーマ」であり、多様な解法を生成できる。証明問題に対するレゾリューション法やPrologの求解問題に対するＳＬＤレゾリューション法などを生み出すばかりか、新しい解法を生み出すことができる。これは、等価変換に基づく解法が問題構造からみて本質的な解法であることを示唆している。
既存のスコーレム化と、我々の提案する「意味保存スコーレム化」とを比較して、関数変数除去という変換を提案し、それが等価変換であることを示した。従来のスコーレム化は、「意味保存スコーレム化」と関数変数除去変換の合成とみなすことができる。関数変数除去変換の適用範囲の狭さにより、既存のスコーレム化の限界を指摘し、「意味保存スコーレム化」を基盤とする解法の汎用性、優秀性を明確に示した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
モデル・インターセクション問題という問題のクラスを新たに導入した。またこの一般クラスに対して等価変換による解法を定式化し、解の正当性を証明した。この解法は、レゾリューション法などより一段高い位置にある「一般スキーマ」であり、多様な解法を生成できる。既存の方法を説明することもできるし、新しい解法を生み出すこともできる。また、既存のスコーレム化の限界を指摘し、「意味保存スコーレム化」を基盤とする解法の汎用性、優秀性を明確に示した。これは今年度の目標を達成している。また多様な論理的問題の研究の新しい強力な基盤を提供することが期待される。
|
| Strategy for Future Research Activity |
モデル・インターセクション問題は、特殊化システムをパラメータとする論理構造に基づく問題クラスであり、特殊化システムを具体的に指定することにより、いろいろなデータ構造を持つ領域に適用できる。次年度はこの理論を、関数変数を含む理論に拡張する。これによって、「意味保存スコーレム化」が切り開いた新しい世界のすべてを受け止める理論を構築できることになる。モデル・インターセクション問題を解く実験システムの増強や新しい問題を解く実験を進め、より大きな問題を高速に解く技術の開発も検討する。
|
| Causes of Carryover |
1月2月に予定していた研究打ち合わせ出張の予定を変更し、システム構築と実験に切り替えたことにより、次年度使用額が生じた。
|
| Expenditure Plan for Carryover Budget |
今年度にできなかった分の研究打ち合わせ出張を次年度に行う。
|
-
-
-
[Presentation] 推論から等価変換へ2016
Author(s)
赤間 清
Organizer
電子情報通信学会（システム数理と応用研究会）
Place of Presentation
海峡メッセ下関(山口県・下関市)
Year and Date
2016-03-03 – 2016-03-04
Invited
