| 研究課題/領域番号 |
15K00003
|
|---|
| 研究機関 | 新潟大学 |
|---|
研究代表者 |
青戸 等人 新潟大学, 自然科学系, 教授 (00293390)
|
|---|
| 研究分担者 |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| キーワード | 項書き換えシステム / 基底合流生 / 書き換え帰納法 |
|---|
| 研究実績の概要 |
帰納的定理の自動証明手法である書き換え帰納法にもとづく基底合流性証明法を考案した．このために，bounded convertibility に基づいて合流性を保証する抽象枠組みを構築し，それに基づいて， 危険対集合のbounded convertibility を書き換え帰納法で証明することにより基底合流性を証明する手法の正しさを証明した．また，(青戸,RTA 2006)の手続きを参考にして，順序付けできない等式を取り扱えるように拡張した基底合流性証明手続きを考案した．その基本的なアイデアは，順序付けできない場合にも，拡大した辺の方向を記録することにより，順序書き換えを利用した簡約化を行う点にある．また，自動証明に適した構成子の選択を行うために，構成子正規項の存在に着目した基礎項書き換え規則の選択戦略を考案し，その戦略にもとづく書き換え帰納法に基づく基底合流性証明システムを実装した．さまざまな具体例を収拾，構築して例題集を作成するとともに，実装システムを用いた実験を行い，提案手法の有効性を確認した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
書き換え帰納法に基づく基底合流性証明の抽象枠組みの構築，順序付けできない等式を取り扱える基底合流性証明手続き，基礎項書き換え規則の選択戦略の考案，基底合流性証明システムの実装と，おおむね計画通りの進捗が得られたため．
|
| 今後の研究の推進方策 |
実装した基底合流性証明システムの実験および評価に取り組み，基礎項書き換え規則の選択戦略および基底合流性証明手続きの改良に取り組む．
|
| 次年度使用額が生じた理由 |
3月支出分が計上されていないため。実際にはワークショップ参加のための旅費および参加費等に支出しているため、残額は20千円弱である。
|
| 次年度使用額の使用計画 |
国際会議参加のための旅費等の補充に充てる。
|
