| 研究課題/領域番号 |
10680346
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 東北大学 (2000-2001)
北陸先端科学技術大学院大学 (1998-1999) |
|---|
研究代表者 |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| 研究分担者 |
草刈 圭一朗 (草刈 圭一郎) 東北大学, 電気通信研究所, 助手 (90323112)
鈴木 大郎 東北大学, 電気通信研究所, 助手 (90272179)
|
|---|
| 研究期間 (年度) |
1998 – 2001
|
| 研究課題ステータス |
完了 (2001年度)
|
| 配分額 *注記 |
1,800千円 (直接経費: 1,800千円)
2001年度: 500千円 (直接経費: 500千円)
2000年度: 500千円 (直接経費: 500千円)
1999年度: 400千円 (直接経費: 400千円)
1998年度: 400千円 (直接経費: 400千円)
|
|---|
| キーワード | 潜在帰納法 / 書き換え帰納法 / 被覆集合帰納法 / 高階 / 書き換えシステム / 完備化 / 項書き換えシステム / 自動証明 |
|---|
| 研究概要 |
プログラム自動検証技術の理論的基礎を与える目的で、潜在帰納法、書き換え帰納法、被覆集合帰納法、および定理自動証明で用いられる関連手法を研究し、理論的解析と実験を通して以下の成果を得た。
(1)潜在帰納法と書き換え帰納法の関係を理論的に解析した。その結果、潜在帰納法がチャーチ・ロッサ性に基づいているのに対し、書き換え帰納法は強正規性に基づいており、この点が両者の最も大きな違いであることが明らかになった。さらに、書き換え帰納法の概念をもちいることにより、被覆集合帰納法を自然に説明できることが示された。
(2)項書き換えシステム、AC-項書き換えシステム、高階書き換えシステムの停止性の証明手法を開発した。ここで提案した新しい手法は、木リフト順序法、改良再帰分解順序法、高階単純順序法、引数フィルタ法、AC-依存対法であり、プログラム検証や定理自動証明の基本技術として有効である。
(3)左右分離型の条件付き線形項書き換えシステムを基礎として、書き換えシステムの新しい線形化手法を提案した。リダクションのステップ数を重みと見なすことで、重み減少合流性の概念を新たに提案した。この概念を利用することにより、左右分離型の条件付きシステムの合流性を保証する十分条件を示した。
|
