| 研究課題/領域番号 |
25330004
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| 研究分担者 |
青戸 等人 東北大学, 電気通信研究所, 准教授 (00293390)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| キーワード | 項書き換えシステム / 合流性 / 定理自動証明 / 自動検証 |
|---|
| 研究実績の概要 |
項書き換えシステムの合流性を自動的に検証する方法を提案し、それに基づいて合流性自動証明システムACPの実装と改良を進めるとともに、プログラム自動検証や定理自動証明に必要となる関連技術を検討した。本年度の主な研究実績は以下のとおりである。
(1) 項書き換えシステムの永続性と型情報を利用した新しい合流性証明法に基づいて、従来手法では困難であった非線型項書き換えシステムの合流性自動証明手続きを実装し、実験をとおしてその有効性を確認した。
(2) 自動検証を目的とした項書き換えシステム自動変換法を提案し、変換の正当性を理論的に証明するとともに、変換を用いた帰納的定理自動証明法の有効性を実験によって明らかにした。
(3) 束縛変数をもつ高階書き換えが可能である名目書き換えシステムの新しい形式化を行い、直交名目書き換えシステムの合流性を保証するための十分条件を明らかにした。
(4) 木オートマトンの完備化に基づく項書き換えシステムの到達可能性の判定手続きを改良し、安定な線形項書き換えシステムに対する到達可能性問題が決定可能となることを明らかにした。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
下記の項目で計画以上の進展があった。
(1) 合流性の自動証明： 項書き換えシステムの永続性と型情報を利用することで、従来は困難であった減少ダイアグラム法による合流性判定が、非線型項書き換えシステムに対しも有効となることを実装と実験をとおして明らかにした。
(2) プログラム自動検証： 自動検証のためのプログラム変換法である文脈移動法と文脈分割法が、項書き換えシステムに対しても有効であるであることを理論的に示すとともに、自動変換と組み合わせた定理自動証明システムを実装し、その有効性を明らかにした。
(3) 高階システムの合流性： 名目書き換えシステムの形式化と合流性の実効的な十分条件を与えた。
(4) 項書き換えシステムの到達可能性： 安定な線形書き換えシステムの到達可能性問題が決定可能となることを明らかにした
|
| 今後の研究の推進方策 |
以下方針で研究を進める。
(1) 合流性の自動判定： 減少ダイアグラム法、危険対解析、階層構造解析、永続性、型情報などを組み合わせることによって、項書き換えシステムのより強力な合流性判定法を開発する。
(2) プログラム自動検証： 書き換え帰納法と項書き換えシステム変換法を組み合わせた高機能なプログラム自動検証法を検討するとともに、プログラムの評価戦略を考慮した検証技術を開発する。
(3) 高階システムの合流性： 名目書き換えシステムの完備化手続きの実現と、それに基づく高階定理自動証明の実験を行う。
(4) 項書き換えシステムの到達可能性： 安定な線形項書き換えシステムのクラスを拡張することにより、より広いクラスに対する到達可能性問題の決定可能性を明らかにする。
|
| 次年度使用額が生じた理由 |
論文の掲載料が当初予定より廉かったため。
|
| 次年度使用額の使用計画 |
次年度に出版予定の論文の掲載料として使用する
|
