| 研究課題/領域番号 |
22500002
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| 研究分担者 |
青戸 等人 東北大学, 電気通信研究所, 准教授 (00293390)
|
|---|
| キーワード | 書き換えシステム / 合流性 / 自動検証 / 停止性 / モジュラ性 |
|---|
| 研究概要 |
項書き換えシステムの合流性を自動的に判定する方法を提案し、それにもとづく合流性自動判定システムのプロトタイプの実装と改良を進めた。本自動判定システムの特徴は、項書き換えシステムを部分システムに分解して合流性を判定する分割統治法を利用している点である。本年度の主な研究実績は以下のとおりである。
(1)項書き換えシステムの合流性が永続性をみたすことを利用して、非線型な項書き換えシステムを線形なシステムに変換して合流性を証明する手法を開発した。さらに、本手法を実装して、分割統治法が適用困難な例題に対して合流性自動判定の実験を行い、本手法の有効性を明らかにした。
(2)項書き換えシステムの可換性は、分割統治法に基づく合流性自動証明で重要な役割をはたしている。そこで、可換性を保証する新しい判定手法として、片側減少ダイアグラム法を開発した。さらに、提案手法にもとづく可換性自動判定システムを実装し、本手法の有効性を示した。
(3)項書き換えシステムに基づく定理自動証明システムを高階システムに拡張する場合、束縛変数の取り扱いは大きな問題となる。そこで、束縛変数の簡明なモデルとして近年活発に研究されている名目システムを調査し、名目書き換えシステムに基づく高階定理自動証明システムの実装を進めた。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
従来よりも強力な合流性自動判定法や可換性自動判定法の開発に成功しており、これらの提案手法の有効性も実験をとおして明かになっている。
|
| 今後の研究の推進方策 |
これまで個別に開発してきた合流性自動判定手法や関連技術を、合流性自動証明システムACPに有機的に統合して、強力な合流性自動証明システムを実現する。
|
