An Extension of the Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems

摘要

This paper explores how to extend the depen- dency pair technique for proving termination of higher-order rewrite systems. We show that the termination property of higher-order rewrite systems can be checked by the non-existence of an infinite R-chain, which is an extension of Arts' and Giesl's result for the first-order case. It is clarified that the subterm property of the quasi-ordering, used for proving termination au- tomatically, is indispensable.