LIFTING OF L-NARROWING DERIVATIONS

If conditional rewrite-rules are restricted to the form P --> f(x(1),. ..,x(n)) --> t where P is a finite set of equations, f is any function symbol, x(1),...,x(n) are variables, and t is any term then the premi se P contains in general variables which do not occur in the list x(1) ,...,x(n). The rule with premise P can be applied if P is satisfiable. Therefore, we need methods to solve P and narrowing must be combined with rewriting. But, narrowing becomes a special case, called L-narrow ing, closely related to lazy-narrowing. Two lifting lemmas are shown w hich characterize the relationship of L-narrowing: derivations if the goals are modified by substitutions. From these lifting lemmas, soundn ess and completeness results can be concluded.