| 研究課題/領域番号 |
22500002
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報学基礎
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| 研究分担者 |
青戸 等人 東北大学, 電気通信研究所, 准教授 (00293390)
|
|---|
| 研究期間 (年度) |
2010 – 2012
|
| 研究課題ステータス |
完了 (2012年度)
|
| 配分額 *注記 |
3,640千円 (直接経費: 2,800千円、間接経費: 840千円)
2012年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2011年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2010年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
|
|---|
| キーワード | 書き換えシステム / 合流性 / 自動検証 / 停止性 / モジュラ性 |
|---|
| 研究概要 |
項書き換えシステムの理論は定理自動証明や計算モデルでひろく利用されている。近年、項書き換えシステムの停止性自動証明システムが数多く開発されているにもかかわらず、合流性自動証明システムについてはほとんど研究されていない。本研究では、さまざまな手法に基いて項書き換えシステムの合流性自動証明システムACPを開発することである。研究成果としては、リダクション保存完備化による合流性自動証明、片側減少ダイアグラムによる可換性自動証明、多項式サイズ正規形を保証する経路順序、永続性をもちいた合流性自動証明などがある。合流性に関する国際ワークショップ(IWC2012)における合流性自動判定システムの第1回コンペティションにおいて、本研究で開発されたACPは、参加3システム中第1位の成績で優勝することができた。
|
