| 研究実績の概要 |
項書き換えシステムは,形式手法に基づくソフトウェア構成・検証技術の基礎を与える重要な計算モデルである. 帰納的定理は,項書き換えシステムをプログラムとして見做したときに成立する性質に対応し,基底合流性は,項書き換えシステムの解析において重要な解の一意性を保証する性質である. 条件付き項書き換えシステムは,ホーン節論理の書き換えシステムによるモデル化であり,関数型プログラムのモデルとして,応用上重要な拡張である. 本研究は,条件付き項書き換えシステムにおける帰納的定理および基底合流性の自動証明・検証理論の基盤構築および証明・検証ツールの実現を目標としている．
本年度は，まず3型指向式条件付き項書き換えシステムにおけるホーン節帰納的定理の自動証明法について取り組んだ．与えられた指向式条件付き項書き換えシステムをアンラベリング変換を用いて項書き換えシステムへ変換し，帰納的定理を項書き換えシステムで証明したときに，どのような条件のもとで，その証明手続きの正しさが成立するのかという問題についての理論的な検討を行った．さらに，書き換え帰納法のおいて，与えられた式がホーン節の場合に適用できるような推論規則を検討した．実装についても取り組み，等式定理の場合と異なり，どのようなヒューリスティクスを適用すればよいかはあまり自明ではないことが判明した．
また，ホーン節帰納的定理の反駁証明や，書き換え帰納法の対話的定理証明器を用いた形式化，また，従来の発散鑑定法では補題の生成が困難な場合の補題生成法，さらに，帰納的定理の決定手続きを書き換え帰納法において利用する手法などについても検討を行なった．
|
