9th International Symposium on Functional and Logic Programming
(FLOPS 2008).
Springer LNCS 4989, pp. 113-129, 2008.
See also the associated
technical
report with proofs.
© Springer-Verlag
Narrowing extends rewriting with logic capabilities by allowing logic variables in terms and replacing matching with unification. Narrowing has been widely used in different contexts, ranging from theorem proving to language design. Surprisingly, the termination of narrowing has been mostly overlooked. In this paper, we present a new approach for analyzing the termination of narrowing in left-linear constructor systems|a widely accepted class of systems|that allows us to reuse existing methods in the literature on termination of rewriting.
Available: PDF / slides / BibTeX entry