プログラム検証のための帰納的定理自動証明法の研究

2001 Fiscal Year Annual Research Report

• Project/Area Number: 10680346
• Research Institution: Tohoku University
• Principal Investigator: 外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
• Co-Investigator(Kenkyū-buntansha): 草刈 圭一朗 東北大学, 電気通信研究所, 助手 (90323112)
• Keywords: 潜在帰納法 / 書き換え帰納法 / 被覆集合帰納法 / 高階 / 書き換えシステム / 完備化

Research Abstract

新しいプログラム検証技術の形式的な基礎を与える目的で、項書き換えシステムに基づく帰納的定理の自動証明手法である潜在帰納法と書き換え帰納法の差異を解析するとともに、自動証明に有効な関連手法を研究し以下の成果を得た。
(1) 被覆集合帰納法と書き換え帰納法で証明可能な命題のクラスを解析した。従来の被覆集合帰納法では、帰納的定理か否かが決定可能な命題は一つの等式の形に制限されており、項書き換えシステムによる関数の定義も相互再帰が許されていなかった。本研究では、これらの制限が命題の決定性を保証する条件としては本質的ではないことを示し、従来の手法では示すことが困難であった決定可能なクラスを明らかにした。また、被覆集合帰納法のかわりに書き換え帰納法をもちいることで、決定可能性問題の解析がはるかに簡明となることを示した。
(2) 定理自動証明やプログラムの正当性検証で重要な高階書き換えシステムのリダクションの停止条件について解析した。従来提案されていた依存対による停止性判定手法は、1階の書き換えシステムの解析には非常に有効であることが知られていた。本研究では、依存対の概念を高階関数に対して拡張することで、同様の判定手法が高階書き換えシステムに対しても適用できることを示した。
(3) 項書き換えシステムの自動合成の実験を行い、完備化手続きを帰納的定理とともにもちいることによって、完備化にもとづくプログラムの自動合成が可能であることを明らかにした。とくに、関数定義がデータ構造に依存している場合には、帰納的定理の自動証明メカニズムがプログラムの自動変換システムの構築に不可欠であることが明らかになった。

Research Products

• [Publications] Yoshihito Toyama: "Equational Proofs by Completion"Journal of Japanese Society for Artificial Intelligence. 16・5. 668-674 (2001)
• [Publications] Keiichirou Kusakari: "On Proring termination of Term Rewriting Systems with Higher-Order Variables"IPSJ Transactions on Programming. 42・SIG7. 35-45 (2001)
• [Publications] Keiichirou Kusakari: "On Proring AC-Termination by AC-Dependency Paris"IEICE Transactions on Information and Systems. E84-D・5. 604-612 (2001)
• [Publications] Yoshihito Toyama: "Church Rosser Property and Unique Normal Form Property of Non Duplicating Term Rewriting Systems"IEICE Transactions on Information and Systems. E84-D・4. 439-447 (2001)