2000 Fiscal Year Annual Research Report
| Project/Area Number |
10680346
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
草刈 圭一郎 東北大学, 電気通信研究所, 助手 (90323112)
鈴木 大郎 東北大学, 電気通信研究所, 助手 (90272179)
|
|---|
| Keywords | 項書き換えシステム / 自動証明 / 潜在帰納法 / 書き換え帰納法 |
|---|
| Research Abstract |
新しいプログラム検証技術の形式的な基礎を与える目的で、項書き換えシステムに基づく帰納的定理の自動証明手法である潜在帰納法と書き換え帰納法の差異を解析するとともに、自動証明に有効な関連手法を研究し以下の成果を得た。
(1)潜在帰納法と書き換え帰納法にそれぞれ反駁証明法を組み合わせた証明能力の等価性について理論的に解析し、それぞれの証明手法の実装上の違いが具体的な自動証明の能力に影響を与えていることを明らかにした。
(2)定理自動証明やプログラムの正当性検証で重要なリダクションの停止条件について解析し、従来提案されていた依存対による停止性判定手法が結合律と交換律をもつような関数に対しても拡張できることを示した。
(3)項書き換えシステムの自動合成の実験を行い、完備化手続きをもちいることによって融合変換にもとづくプログラムの自動合成が可能であることを明らかにした。
|
-
[Publications] K.Kusakari: "On Proving AC-termination by AC-dependency Paiks"信学会論文誌. (発表予定).
-
[Publications] Y.Toyama: "Church-Rosser property and unique normal form property of non-duplicating term rewriting systems"信学会論文誌. (発表予定).
-
[Publications] 小池広高: "潜在帰納法と書換え帰納法の比較"コンピュータソフトウェア. 17. 1-12 (2000)
-
[Publications] Y.Toyama: "New challenges for computational models (Pcs.Statement)"Lecture Notes in Comput Sci.. 1872. 612-613 (2000)
-
[Publications] K.Kusakari: "On proving AC-termination by argument filtering method"IPSJ.Trams.On Programming. 41. 65-78 (2000)
