プレスブルガー文付き項書換え系における書換え帰納法について

摘要

手続き型プログラムを等価な制約付き項書換え系に変換してプログラム等価性を検証する手法の研究において，潜在帰納法と呼ばれる手法が制約付き項書換え系に対応するように拡張されている．しかし，潜在帰納法と同じく帰納的定理を証明する手法である書換え帰納法は制約付き項書換え系に対応するように拡張されていない．本論文では，制約付き項書換え系に対応するように書換え帰納法を拡張し，それに基づいた帰納的定理の定理自動証明法を提案する．また，制約をプレスブルガー文に限定した場合に，潜在帰納法よりも簡潔に証明できる例を紹介する．