2015 Fiscal Year Annual Research Report
| Project/Area Number |
25330004
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
青戸 等人 新潟大学, 自然科学系, 教授 (00293390)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | 項書き換えシステム / 合流性 / 定理自動証明 / 自動検証 |
|---|
| Outline of Annual Research Achievements |
項書き換えシステムの合流性を自動的に検証する方法を提案し，それに基づいて合流性自動証明システムACPの実装と改良を進めるとともに，プログラム自動検証や定理自動証明に必要となる関連技術を検討した．本年度の主な研究実績は以下のとおりである．
(1) 項書き換えシステムの永続性と型情報を利用した新しい合流性証明法に基づいて、従来では困難であった非線型項書き換えシステムに対しも、減少ダイアグラム法による合流性判定が有効となることを明らかにした。(2) 項書き換えシステムの基底合流性を書き換え帰納法に基づいて自動証明する新しい手法を提案するとともに、その有効性を実験をとおして明らかにした。(3) 自動検証を目的としたプログラム変換法である文脈移動法が、項書き換えシステムの自動変換にも有効であることを明らかにするとともに，先行評価における文脈移動法の正当性を理論的に証明した。(4) 束縛変数をもつ高階書き換えが可能である名目書き換えシステムの新しい形式化を提案し，名目書き換えシステムの合流性を保証するための十分条件を危険対解析に基づいて明らかにした。(5) 整礎順序をもつモノイド上での抽象リダクションシステムの理論を構築し、この理論が項書き換えシステムの正規戦略の解析に極めて有効であることを明らかにした。
|
