| 研究課題/領域番号 |
22700009
|
|---|
| 研究種目 |
若手研究(B)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
情報学基礎
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
廣川 直 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (50467122)
|
|---|
| 研究協力者 |
ミデルドープ アート University of Innsbruck, Institute for Computer Science, Professor
クライン ドミニク 北陸先端科学技術大学院大学, 情報科学研究科, 博士後期課程学生(当時)
|
|---|
| 研究期間 (年度) |
2010 – 2012
|
| 研究課題ステータス |
完了 (2012年度)
|
| 配分額 *注記 |
3,770千円 (直接経費: 2,900千円、間接経費: 870千円)
2012年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2011年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2010年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
|
|---|
| キーワード | 項書換え / 合流性 / 完備化 / 戦略 / 計算理論 / 関数型プログラム |
|---|
| 研究概要 |
本研究では関数型プログラムや定理証明システムの計算モデルである項書換えシステムに対し、その基礎理論を相対停止性という性質をもとに再考した。その研究成果として、合流性に関する主要二定理(Rosen の直交性と完備性)を左線形の場合に対し統一した。また極大完備化という定理証明ための新たな基盤技術を開発した。これらの新技法を採用した強力な合流性解析ツールSaigawa と自動完備化ツールMaxcomp を開発した。
|
