制約付き項書換え系の書換え帰納法における補題等式の自動生成法

摘要

近年，帰納的定理の証明原理の1つである書換え帰納法が制約付き項書換え系に対応するように拡張され，命令型プログラムの等価性検証に応用するための枠組みが提案された．帰納的定理の証明のためには適切な補選等式を与える必要がある場合が多いが，項書換え系においてこれまで研究が進んでいる補題生成の手法を制約付き項書換え系に対して利用するためには制約部分を扱うための拡張が必要である．本論文では，書換え規則から項の関係を定式化し，その関係に基づいて等式をより一般的な等式に変換する枠組みを提案する．さらに，制約付き項書換え系の書換え帰納法による証明手続きにその枠組みを利用した補選等式の生成・追加機能を組み込むことで，補選等式を予め記述せずに定理自動証明を試み，その有効性を検証する．