| 研究課題/領域番号 |
23500002
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
青戸 等人 東北大学, 電気通信研究所, 准教授 (00293390)
|
|---|
| 研究分担者 |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| 研究期間 (年度) |
2011-04-28 – 2014-03-31
|
| キーワード | 項書き換えシステム / 自動定理証明 / 帰納的定理 / 補題発見 |
|---|
| 研究概要 |
本研究の目的は書き換えシステムに基づく帰納的定理の自動証明法において、証明能力の向上に資する補題発見法およびその基盤となる補題生成法を高度化を試みることである。本年度は、アイデアの基盤となる技術について調査を行うとともに補題発見法への応用の基盤となる理論の構築を複数の着想点から行った。まず、反復的なプログラムから再帰的なプログラムへの変換手法において、その等価性を暗黙帰納法を用いて保証する枠組みを与えた。これによりパターンに基づく変換や文脈保存を正当性と切り離して議論できる。また、発散から生じる等式からの補題生成への応用を見込んで、正則項書き換えの基礎理論の構築を行った。特にオートマトン理論を用いて書き換えステップの決定可能性を与えた。また、正則項との関連から半単一化について調査を行い、正則項上の単一化と半単一化の関連性を明らかにした。決定可能性理論を応用するために組み込みデータ型をもつ書き換えシステムの始代数意味論について検討を行った。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
当初に計画していた複数の着想点から補題発見法への応用の基盤となる理論の構築が進めることが出来ており、おおむね順調に進展しているといえる。
|
| 今後の研究の推進方策 |
進展した着想点のそれぞれについて以下のような推進方策は以下の通りである。(1) 発散を生じる等式集合からの補題生成。 引き続き、正則項および半単一化との関連から考察を進める。(2) 公理の等価性に基づく補題生成とパターンに基づく補題生成。 本年度の研究から暗黙帰納法の異なる原理を組み合わせることで、これら2つの着想点を組み合わせた補題生成法が可能なのではないかという着想が得られた。このアプローチに基づいて考察を進める。(3) 決定可能性理論を応用した補題生成法。 組み込みデータ型をもつ書き換えシステムの始代数意味論について更に検討を進め、基盤理論の構築を試みる。
|
| 次年度の研究費の使用計画 |
現在のところ、当初の計画からの大幅な変更は予定していない。
|
