Narrowing Directed by a Graph of Terms

9 years 21 days ago
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.
Jacques Chabin, Pierre Réty
Added 27 Aug 2010
Updated 27 Aug 2010
Type Conference
Year 1991
Where RTA
Authors Jacques Chabin, Pierre Réty
Comments (0)