Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
7 References
Jacques Chabin. Surréduction dirigée par un graphe d'opérateurs. Formulation équitable par des systèmes d'équations et implantation. Rapport de DEA, université d'Orléans, Septembre 1990. (In french).
J. Chabin and P. Réty. Narrowing directed by a graph of terms (including proofs). Internal report 91-1, LIFO, Université d'Orléans. 1991.
N. Dershowitz and G. Sivakumar. Solving goals in equational langages. Proceedings of the first workshop CTRS. Springer-Verlag, vol 308. 1987.
N. Dershowitz and J.P. Jouannaud. Rewrite system. Handbook of Theoretical Computer Science, Vol B, North-Holland, 1990.
M. Fay. First-Order Unification in an Equational Theory. Master Thesis 78-5-002. University of Santa Cruz. 1978.
J.A. Goguen and J. Meseguer. EQLOG: Equality, Types and generic Modules for logic Programming. In logic programming: functions, relations and equations. D. Degroot and G. Lindstrom, eds. Prentice-Hall, Englewood Cliffs, NJ, pp 295–363, 1986.
A. Herold. Narrowing Techniques applied to idempotent Unification. Internal SEKI Report SR-86-16. August 1986.
J.M. Hullot. Canonical forms and unification. Proceedings of the fifth Conference on Automated Deduction, Springer-Verlag, vol 87, July 1980.
C. Kirchner. A new equational unification method: a generalization of Martelli-Montanari's algorithm. Proceedings of the 7th CADE. Springer-Verlag, vol 170. 1984.
A. Martelli, C. Moiso, and G-F. Rossi. Lazy unification algorithms for canonical rewrite systems. Proceedings of CREAS, Austin, Texas. May 1987.
P. Réty. Improving basic Narrowing Techniques. Proceedings of the second conference on Rewriting Techniques and Applications, Springer-Verlag, vol 256. May 1987.
G. Sivakumar and N. Dershowitz. Goal directed equation solving. Technical report. University of Illinois, USA. 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chabin, J., Réty, P. (1991). Narrowing directed by a graph of terms. In: Book, R.V. (eds) Rewriting Techniques and Applications. RTA 1991. Lecture Notes in Computer Science, vol 488. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53904-2_90
Download citation
DOI: https://doi.org/10.1007/3-540-53904-2_90
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53904-9
Online ISBN: 978-3-540-46383-2
eBook Packages: Springer Book Archive