@article{oai:nagoya.repo.nii.ac.jp:00018994,
 author = {笹田, 悠司 and 酒井, 正彦 and 西田, 直樹 and 坂部, 俊樹 and 草刈, 圭一朗 and SASADA, Yuji and SAKAI, Masahiko and NISHIDA, Naoki and SAKABE, Toshiki and KUSAKARI, Keiichiro},
 issue = {176},
 journal = {電子情報通信学会技術研究報告SS, ソフトウェアサイエンス},
 month = {Jul},
 note = {システムがどのように外部観測的に振舞うかを規定する振舞仕様の下で、観測を通してシステムの2つの状態が等しいことを振舞等価という。振舞等価性の自動証明法の一つに、潜在帰納法に基づく証明法が提案されている.しかし,この手法では簡約化順序で順序付けができない2つの項が存在するとき振舞等価性の証明に失敗する。本論文では、このような場合にも証明できるようにするために、等式付き書換えを用いた潜在帰納法に基づく証明法を提案する。さらに,完全な仕様の場合には手続き中の条件を判定可能な十分条件に置き換えられることを示す., A behavioral specification is a description of what is supposed to happen. Two states are said to be behaviourally equivalent on a behavioral specification if they are observationally indistinguishable. A proof method based on implicit induction principle have been proposed as an automatic proof method for behavioral equivalence. However it is a problem that the method sometimes fails to prove when two terms that represent states cannnot be ordered by the given reduction order. This paper proposes an implicit induction proof-method based on equational rewriting in order to solve the above problem. We also show a decidable sufficient condition for the context reducibility that used in the procedure.},
 pages = {7--12},
 title = {振舞等価性の証明のための等式付き書換えに基づく潜在帰納法},
 volume = {107},
 year = {2007}
}