On New Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems
Masahiko Sakai, Keiichirou Kusakari · Institutional Repositories DataBase (IRDB) · 2001
This paper explores how to extend the dependency pair technique for proving termination of higher-order rewrite systems. We introduced a new notion of dependency forest and show that the termination property of higher-order rewrite systems R can be checked by the non-existence of an infinite R-chain, if R is non-duplicating or non-nested. One benefit is we can exclude any term whose top symbol is higher order variable from the second item of dependency pair.