| 研究課題/領域番号 |
15K00003
|
|---|
| 研究機関 | 新潟大学 |
|---|
研究代表者 |
青戸 等人 新潟大学, 自然科学系, 教授 (00293390)
|
|---|
| 研究分担者 |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| キーワード | 項書き換えシステム / 基底合流性 / 書き換え帰納法 |
|---|
| 研究実績の概要 |
昨年度に考案した帰納的定理の自動証明手法である書き換え帰納法にもとづく基底合流性証明法の改良を行なった．まず，関数定義に必要な書き換え規則が含まれていない場合に，それを構成する手続きを導入した．それぞれの関数の定義において，定義されていないパターンを検出し，そのパターンに対する適当な書き換え規則を探索することで，適切な関数定義を補完する手法を考案した．不足パターンの検出には補パターンアルゴリズムを用いた．また，関数定義がある場合でも，停止性をもたない等の書き換え帰納法の利用に適さない規則である場合には，書き換え帰納法に適した規則を追加することで，より本手法の適用範囲を広げることに成功した．次に，より柔軟なデータ構造に対する項書き換えシステムを扱うために，順序付け不能な構成子規則を取扱うための拡張を行なった．このために，書き換え帰納法の導出システムを拡張するとともに，導出の正当性を保証するための十分条件を与えた．なお，この十分条件(定義規則の左線形性)は，実際のツールでは適切な証明戦略の一環としてに組み込まれるものであるため，本手法を大きく制約するものではない．線形代入のアイデアを用いて，構成子規則についても，書き換え規則の変換を組み合わせる手法も考案した．最後に，基底合流性の反証法を考案した．反証のために，書き換え帰納法に反証のための規則を導入し，書き換え帰納法の途中でも効率的に反証を行う機能を加えた．また，合流性反証法を基底合流性反証に応用した，より強力な反証法も考案した．また，これらの改良を実装し，提案手法の有効性を確認した.
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
昨年度考案した書き換え帰納法にもとづく項書き換えシステムの基底合流性の自動証明法において，関数定義の補完法，順序付け不能な構成子規則の扱い法，反証機能の導入，という大きく3つの改良を考案することができたため．
|
| 今後の研究の推進方策 |
改良した基底合流性証明システムの実装をより洗練するとともに，より難易度の高い問題に対する実験および評価に取り組み,より強力な基底合流性証明システムを構築する．
|
