2015 Fiscal Year Research-status Report
| Project/Area Number |
15K00003
|
|---|
| Research Institution | Niigata University |
|---|
Principal Investigator |
青戸 等人 新潟大学, 自然科学系, 教授 (00293390)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | 項書き換えシステム / 基底合流生 / 書き換え帰納法 |
|---|
| Outline of Annual Research Achievements |
帰納的定理の自動証明手法である書き換え帰納法にもとづく基底合流性証明法を考案した．このために，bounded convertibility に基づいて合流性を保証する抽象枠組みを構築し，それに基づいて， 危険対集合のbounded convertibility を書き換え帰納法で証明することにより基底合流性を証明する手法の正しさを証明した．また，(青戸,RTA 2006)の手続きを参考にして，順序付けできない等式を取り扱えるように拡張した基底合流性証明手続きを考案した．その基本的なアイデアは，順序付けできない場合にも，拡大した辺の方向を記録することにより，順序書き換えを利用した簡約化を行う点にある．また，自動証明に適した構成子の選択を行うために，構成子正規項の存在に着目した基礎項書き換え規則の選択戦略を考案し，その戦略にもとづく書き換え帰納法に基づく基底合流性証明システムを実装した．さまざまな具体例を収拾，構築して例題集を作成するとともに，実装システムを用いた実験を行い，提案手法の有効性を確認した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
書き換え帰納法に基づく基底合流性証明の抽象枠組みの構築，順序付けできない等式を取り扱える基底合流性証明手続き，基礎項書き換え規則の選択戦略の考案，基底合流性証明システムの実装と，おおむね計画通りの進捗が得られたため．
|
| Strategy for Future Research Activity |
実装した基底合流性証明システムの実験および評価に取り組み，基礎項書き換え規則の選択戦略および基底合流性証明手続きの改良に取り組む．
|
| Causes of Carryover |
3月支出分が計上されていないため。実際にはワークショップ参加のための旅費および参加費等に支出しているため、残額は20千円弱である。
|
| Expenditure Plan for Carryover Budget |
国際会議参加のための旅費等の補充に充てる。
|
