2016 Fiscal Year Annual Research Report
From "proof"+"inference" to "query-answering problems" + "equivalent transformation"
| 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 |
従来の論理計算の理論体系は、一階述語論理式で書かれた証明問題を推論によって解くことが基本になっている。しかし、解くことのできる証明問題は、組み込み述語を使わないものに限られている。さらに求解問題を解く理論も十分でない。従来の論理と計算の枠組みは、構造的に不十分なのである。
本研究課題の挑戦は、証明問題中心の理論を脱皮して、求解問題中心の理論へ、そしてモデルインターセクション問題中心の理論へ拡大飛躍することである。本研究では、① 新しいロジックであるＫＲロジック、② 新しい問題クラスであるモデルインターセクション問題、③ 新しい計算を生み出す等価変換、という枠組みを確立し、既存の論理計算の理論を一新することに成功した。論理式やモデルという最も基本的な定義も改定し、問題クラスも拡大し、計算の概念も拡大された。節の概念も拡張され、論理式から節集合への変換は、充足可能性のみならず、論理式の意味をも保存する等価変換となった。既存の「証明問題＋推論」は新しい「モデルインターセクション問題＋等価変換」の一部としてとらえることができる。
今年度の主要な研究は、関数変数が入ったＫＲロジックのもとでモデルインターセクション問題を定式化し、それを等価変換で解く一般スキーマを与えたことと、その新しいロジックのもとで、アンフォールド変換などの主要な変換を定義し、それが等価変換であることを証明したことである。これは本研究の核の部分を完成し、今後の着実な発展の基礎を与える重要な成果である。
この理論は論理学と論理計算を歴史的に新たな段階へと引き上げるものである。それは一般性と明快性によって、論理計算の理論と応用のさらなる発展に貢献する。また、アルゴリズム発見やプログラム自動構築など、論理と計算における未解決の難問に挑戦するためになくてはならない基礎を与えるものである。
|
