Narrowing Directed by a Graph of Terms

Narrowing provides a complete procedure to solve equations modulo confluent and terminating rewriting systems. But it seldom terminates. This paper presents a method to improve the termination. The idea consists in using a finite graph of terms built from the rewriting system and the equation to be solved, which helps one to know the narrowing derivations possibly leading to solutions. Thus, the other derivations are not computed. This method is proved complete. An example is given and some improvements are proposed.

• Type: Conference
• Year: 1991
• Where: RTA
• Authors: Jacques Chabin, Pierre Réty
• Keywords: Narrowing Derivations, Rewriting System, RTA 1991, Terminating Rewriting Systems, Theoretical Computer Science