Dependency Graph Method for Proving Termination of Narrowing
Miura Koichi, Naoki Nishida, Masahiko Sakai, Keiichirou Kusakari, Toshiki Sakabe · IEICE Technical Report; IEICE Tech. Rep. · 2005
Term rewriting systems with extra variables are useful in encoding operators for inverse compu- tation. Their ground rewrite sequences can be simulated by narrowing sequences. In this paper, we reflne the dependency pair method for proving termination of narrowing and extend the dependency graph method for proving termination of rewriting to a method for narrowing.