@inproceedings{oai:nagoya.repo.nii.ac.jp:00019062,
 author = {中林, 直生 and 西田, 直樹 and 草刈, 圭一朗 and 坂部, 俊樹 and 酒井, 正彦 and Nakabayashi, Naoki and Nishida, Naoki and Kusakari, Keiichirou and Sakabe, Toshiki and Sakai, Masahiko},
 month = {Sep},
 note = {近年，帰納的定理の証明原理の一つである書換え帰納法が制約付き項書換え系に対応するように拡張され，命令型プログラムの等価性検証に応用するための枠組みが提案された．帰納的定理の証明のためには適切な補題等式を与える必要がある場合が多いが，これまで研究が進んでいる項書換え系に対する補題生成の手法は制約付き項書換え系に対してはあまり有効ではない．本論文では，書換え規則から項の関係を定式化し，その関係に基づいて等式をより一般的な等式に変換する枠組みを提案する．さらに，制約付き項書換え系の書換え帰納法による証明手続きにその枠組みを利用した補題等式の生成・追加機能を組み込むことで，補題等式を予め記述せずに定理自動証明を試み，その有効性を検証する．, 日本ソフトウェア科学会第26回大会講演論文集 (2009年9月16日(水)～9月18日(金), 島根大学)},
 publisher = {日本ソフトウェア科学会},
 title = {制約付き項書換え系の書換え帰納法における補題等式の自動生成法},
 year = {2009}
}