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.
CITATION STYLE
Chabin, J., & Réty, P. (1991). Narrowing directed by a graph of terms. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 488 LNCS, pp. 112–123). Springer Verlag. https://doi.org/10.1007/3-540-53904-2_90
Mendeley helps you to discover research relevant for your work.