Sciweavers

AAECC
2010
Springer

Termination of narrowing via termination of rewriting

13 years 11 months ago
Termination of narrowing via termination of rewriting
Abstract Narrowing extends rewriting with logic capabilities by allowing logic variables in terms and by replacing matching with unification. Narrowing has been widely used in different contexts, ranging from theorem proving (e.g., protocol verification) to language design (e.g., it forms the basis of functional logic languages). Surprisingly, the termination of narrowing has been mostly overlooked. In this work, we present a novel 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. Keywords narrowing, term rewriting, termination Mathematics Subject Classification (2000) 68N17
Naoki Nishida, Germán Vidal
Added 08 Dec 2010
Updated 08 Dec 2010
Type Journal
Year 2010
Where AAECC
Authors Naoki Nishida, Germán Vidal
Comments (0)