@article{oai:nagoya.repo.nii.ac.jp:00019048,
 author = {服部, 達哉 and 酒井, 正彦 and 西田, 直樹 and 草刈, 圭一朗 and 坂部, 俊樹 and HATTORI, Tatsuya and SAKAI, Masahiko and NISHIDA, Naoki and KUSAKARI, Keiichirou and SAKABE, Toshiki},
 issue = {336},
 journal = {電子情報通信学会技術研究報告SS, ソフトウェアサイエンス},
 month = {Dec},
 note = {順方向ナローイングに基づく非停止性証明解析はAProVE等の停止性証明ツールに採用されている.しかしながら,それが完全である項書換え系のクラス,すなわち,非停止性をもつならば順方向ナローイングに基づく解析でそれが証明可能となるクラスは知られていない.本論文では,依存対が右線形右シャローである項書換え系においては,順方向ナローイングに基づく解析が完全であることを示す., Detecting non-termination of term rewriting systems based on forward narrowing is used in termination tools such as AProVE. However, there is no known class of term rewriting systems for which the detection method is complete, that is, non-termination is always proved by the method. This paper proves that the detection method is complete for the term rewriting systems whose dependency pairs are right-linear and right-shallow.},
 pages = {31--36},
 title = {順方向ナローイングに基づく右線形右シャロー項書換え系の非停止性証明について},
 volume = {110},
 year = {2010}
}