| 研究課題/領域番号 |
19500003
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報学基礎
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| 研究分担者 |
青戸 等人 東北大学, 電気通信研究所, 准教授 (00293390)
|
|---|
| 研究期間 (年度) |
2007 – 2009
|
| 研究課題ステータス |
完了 (2009年度)
|
| 配分額 *注記 |
3,770千円 (直接経費: 2,900千円、間接経費: 870千円)
2009年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2008年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2007年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
|
|---|
| キーワード | プログラム理論 / プログラム変換 / 情報基礎 / 定理自動証明 / 書き換えシステム / 書き換え帰納法 / 融合変換 / 変換パターン / 補題自動導入法 |
|---|
| 研究概要 |
定理自動証明や計算モデルで広く利用されている項書き換えシステムの理論に基づいて、プログラム自動変換を実現するための基礎理論と実験システムを開発した。研究成果としては、プログラム変換のための変換パターン自動抽出アルゴリズムの提案と実験システムの構築、高階プログラムの新しい停止性証明法の提案、書き換え帰納法のための補題自動導入アルゴリズムの提案と実験システムの構築、分割統治法による項書き換えシステムの合流性自動判システムの開発を行った。
|
