| 研究課題/領域番号 |
25540003
|
|---|
| 研究種目 |
挑戦的萌芽研究
|
| 配分区分 | 基金 |
|---|
| 研究分野 |
情報学基礎理論
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
小川 瑞史 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (40362024)
|
|---|
| 研究協力者 |
Christian Sternagel インスブルック大学, ポスドク
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| 研究課題ステータス |
完了 (2015年度)
|
| 配分額 *注記 |
3,770千円 (直接経費: 2,900千円、間接経費: 870千円)
2015年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2014年度: 2,210千円 (直接経費: 1,700千円、間接経費: 510千円)
2013年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
|
|---|
| キーワード | 形式証明 / 計算的意味 / 項書換え系 / 合流性 / 構成的証明 / 定理証明系 / 数理論理 / 古典論理 |
|---|
| 研究成果の概要 |
古典的存在証明からの計算的意味の抽出について、未解決問題を含む決定問題の難問に対する証明構造のケーススタディを行った。「右線形かつ強無曖昧な項書換え系は合流性を持つ」(RTA open problem 58) は、可算選択公理を用いた停止順序の存在は証明できるが、具体的な順序の構成が困難なため未解決問題である。順序の構成条件の精査と、有限リダクショングラフによる構成的証明に基づき、二つの異なる新たな部分クラスに対し、肯定的結果を得た。また、最近、散見される決定問題の難問に対する二つのyes/noをそれぞれ決定する準アルゴリズムを並行させる証明手法について、一般化の考察を進めた。
|
