@article{oai:nagoya.repo.nii.ac.jp:00007859,
 author = {SAKAI, Masahiko and KUSAKARI, Keiichirou},
 issue = {3},
 journal = {IEICE Transactions on Information and Systems},
 month = {Mar},
 note = {This paper explores how to extend the dependency pair technique for proving termination of higher-order rewrite systems. In the first order case, the termination of term rewriting systems are proved by showing the non-existence of an infinite R-chain of the dependency pairs. However, the termination and the non-existence of an infinite R-chain do not coincide in the higher-order case. We introduce a new notion of dependency forest that characterize infinite reductions and infinite R-chains, and show that the termination property of higher-order rewrite systems R can be checked by showing the non-existence of an infinite R-chain, if R is strongly linear or non-nested.},
 pages = {583--593},
 title = {On Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems},
 volume = {E88-D},
 year = {2005}
}