|
項書き換えシステムの基底合流性は，書き換えシステムに基づくソフトウェア検証法を構築する上で基礎となる性質である．本研究では，帰納的定理証明に用いられる書き換え帰納法に着目し，書き換え帰納法において束縛的変換可能性を保証すれば，基底合流性が成立することを示した．そして，束縛的変換可能性を保証する書き換え帰納法を設計して，その理論的な正当性の証明を与えた．また，書き換え規則の変換に基づく適切な関数定義の補完手法，順序付け不能な構成子規則を扱うための推論規則の拡張，基底合流性の反証法などの改良や拡張を考案した．そして，提案手法にもとづく基底合流性自動証明ツールAGCPを開発した．
|
