| 研究課題/領域番号 |
15K00003
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報学基礎理論
|
|---|
| 研究機関 | 新潟大学 |
|---|
研究代表者 |
青戸 等人 新潟大学, 自然科学系, 教授 (00293390)
|
|---|
| 研究分担者 |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| 研究課題ステータス |
完了 (2017年度)
|
| 配分額 *注記 |
4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円)
2017年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
2016年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
2015年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
|
|---|
| キーワード | 項書き換えシステム / 基底合流性 / 書き換え帰納法 / 基底合流生 |
|---|
| 研究成果の概要 |
項書き換えシステムの基底合流性は，書き換えシステムに基づくソフトウェア検証法を構築する上で基礎となる性質である．本研究では，帰納的定理証明に用いられる書き換え帰納法に着目し，書き換え帰納法において束縛的変換可能性を保証すれば，基底合流性が成立することを示した．そして，束縛的変換可能性を保証する書き換え帰納法を設計して，その理論的な正当性の証明を与えた．また，書き換え規則の変換に基づく適切な関数定義の補完手法，順序付け不能な構成子規則を扱うための推論規則の拡張，基底合流性の反証法などの改良や拡張を考案した．そして，提案手法にもとづく基底合流性自動証明ツールAGCPを開発した．
|
