| 研究課題/領域番号 |
23500002
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報学基礎
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
青戸 等人 東北大学, 電気通信研究所, 准教授 (00293390)
|
|---|
| 研究分担者 |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| 研究期間 (年度) |
2011 – 2013
|
| 研究課題ステータス |
完了 (2013年度)
|
| 配分額 *注記 |
5,070千円 (直接経費: 3,900千円、間接経費: 1,170千円)
2013年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2012年度: 2,340千円 (直接経費: 1,800千円、間接経費: 540千円)
2011年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
|
|---|
| キーワード | 項書き換えシステム / 自動定理証明 / 帰納的定理 / 補題発見 |
|---|
| 研究概要 |
書き換えシステムに基づく帰納的定理の自動証明における補題生成法について、補題候補の発見法や補題決定に有効な技術に資する成果を得た。主な研究成果としては、発散を生じる等式を解析するための基礎理論として、正則項の単一化および書き換え理論、半単一化についての理論について新しい知見を与えた。補題の決定手続きに適した書き換え帰納法の決定理論を拡張するとともに、書き換え帰納法において有効な補題決定手続きについて、始代数を用いるアプローチに基づく新しい手続きを考案した。また、書き換えシステムにおける末尾再帰を用いた関数定義において、自動証明に適した関数定義を得るための補題を抽出する手法を考案した。
|
