2013 Fiscal Year Annual Research Report
| Project/Area Number |
23500002
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
青戸 等人 東北大学, 電気通信研究所, 准教授 (00293390)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| Keywords | 項書き換えシステム / 自動定理証明 / 帰納的定理 / 補題発見 |
|---|
| Research Abstract |
本研究の目的は書き換えシステムに基づく帰納定理の自動証明において，証明技術の向上に資する補題発見法およびその基盤となる補題生成法の高度化を試みることである．本年度の主な成果は以下の通りである．
発散から生じる等式からの補題生成については，半単一化問題のグラフを用いた効率的なアルゴリズムの性質を調べるために抽象完備化の枠組みを応用する着想を得て，抽象完備化の調査および単一化問題のグラフアルゴリズムを抽象完備化の枠組みでの形式化について検討を行った．
書き換え帰納法に基づく帰納的定理証明に有効な補題決定手続きについて，従来とは異なる始代数を用いるアプローチに基づき，いくつかの理論について，書き換え帰納法等の定理証明手続きを用いない決定手続きを考案し，その正当性を証明した．
パターンに基づく補題生成については，文脈移動法と文脈分割法を書き換え帰納法に基づく帰納的定理証明を組み合わせた実験システムを構築し，文脈移動法と文脈分割法の帰納的定理証明における有効性を検証した．
以下に3年間の主な研究成果をあげる．半単一化や有理項といった発散構造からの情報抽出に関係する理論について考察を行い，解析に有用と考えられる技術をいくつか得ることが出来た．複数の基本的な等式理論において補題の決定手続きを考案し，書き換え帰納法などの帰納的定理証明において補題を貪欲的に検証するための基礎技術を考案した．末尾再帰プログラムにおいてプログラムの形から文脈移動法と文脈分割法を適用するための補題を抽出するとともに，補題の検証と末尾再帰プログラムにおける帰納的定理証明の組み合わせの有効性を検証した．以上により，書き換えシステムに基づく帰納定理の自動証明において，複数の着想点から補題生成および補題証明に有効な技術が得られるともに，帰納的定理自動証明システムの能力の高度化に資する成果が得られた
|
