| 研究成果の概要 |
項書き換えシステムは,形式手法に基づくソフトウェア構成・検証技術の基礎を与える重要な計算モデルである. 帰納的定理は,項書き換えシステムをプログラムとして見做したときに成立する性質に対応し,基底合流性は,項書き換えシステムの解析において重要な解の一意性を保証する性質である. 条件付き項書き換えシステムは,ホーン節論理の書き換えシステムによるモデル化であり,関数型プログラムのモデルとして,応用上重要な拡張である.本研究では，指向式条件付き項書き換えシステムにおけるホーン節帰納的定理証明のための書き換え帰納法，指向式条件付き項書き換えシステムの基底合流性検証法，階層可換性の十分条件などを与えた．
|
