| 研究課題/領域番号 |
23500002
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
青戸 等人 東北大学, 電気通信研究所, 准教授 (00293390)
|
|---|
| 研究分担者 |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| キーワード | 項書き換えシステム / 自動定理証明 / 帰納的定理 / 補題発見 |
|---|
| 研究概要 |
本研究の目的は書き換えシステムに基づく帰納定理の自動証明において，証明技術の向上に資する補題発見法およびその基盤となる補題生成法の高度化を試みることである．本年度の成果は以下の通りである．
発散から生じる等式からの補題生成については，半単一化を用いて発散パターンを抽出の可能性について検討するため，半単一化について調査を行った．その結果，従来の提案されている手続きの形式推論体系にもとづく部分に厳密な考察がなされていないことが判明した．そこで，半単一化問題についての形式推論体系にもとづく解法を考案し，従来の形式推論体系では半単一化手続きが停止しない場合があることを明らかにするとともに，与えた形式体系において反駁完全性をもつ場合には手続きが必ず停止することを示した．また，反駁完全性をもつ具体的な計算戦略を与えた．書き換え帰納法に基づく帰納的定理の決定手続きについて，その基本原理を整理するとともにその適用条件を明らかにした．特に，従来の提案されていた外山(2001)および(Falke&Kapur,2006)を組み合わせたより柔軟な条件においても帰納的定理が決定可能となることを示した．また，帰納的定理自動証明システムSPIKEの開発者であるSorin~Stratulat氏を訪問し，組み込みデータ型をもつ書き換え帰納法における補題生成および決定手続きを利用した補題生成法について研究討論を行なった．パターンに基づく補題生成を目指して，文脈移動法にもとづくプログラム変換法を書き換えシステムに適用するための基礎的な枠組みについて検討した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
当初に計画していた複数の着眼点から補題発見法への応用の基盤となる理論の構築を進めることが出来ており，おおむね順調に進展している．
|
| 今後の研究の推進方策 |
進展した着想点のそれぞれについて以下の推進方策に取り組む．
(1) 発散を生じる等式集合からの補題生成．半単一化を用いた発散パターン抽出手続きの実装にとり組み，発散パターンからの補題生成法を検討する．
(2) 決定可能性理論を応用した補題生成法．書き換え帰納法に基づく決定手続きや組み込みタ型の決定手続きを検討し，決定手続き内での補題生成や決定手続きの適用可能部分との差分情報を利用した補題生成法について検討を行う．
(3) パターンに基づく補題生成．パターンを用いた項書き換えシステム変換の枠組みを用いて文脈移動法を形式化する手法について検討する．
|
| 次年度の研究費の使用計画 |
当初の計画通り，研究打ち合わせおよび成果発表のための国内旅費，成果発表のための外国旅費および各種会議費に支出する予定である
|
