| 研究課題/領域番号 |
25330004
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報学基礎理論
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| 研究分担者 |
青戸 等人 新潟大学, 自然科学系, 教授 (00293390)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| 研究課題ステータス |
完了 (2015年度)
|
| 配分額 *注記 |
4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円)
2015年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
2014年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
2013年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
|
|---|
| キーワード | 項書き換えシステム / 合流性 / 定理自動証明 / 自動検証 |
|---|
| 研究成果の概要 |
項書き換えシステムの理論は定理自動証明や計算モデルで広く利用されている。近年、項書き換えシステムの合流性自動証明システムがいくつか開発されているが、合流性自動証明システムの応用ついてはほとんど研究されていない。本研究では、項書き換えシステムの合流性自動証明システムに基づくプログラム自動検証法を研究する。研究成果としては、永続性と型情報に基づく合流性判定、プログラム変換に基づく定理自動証明、名目書き換えシステムの合流性条件、木オートマトン完備化の停止条件、基底合流性の自動判定、整礎順序をもつモノイド上の抽象リダクションシステムなどがある。
|
