Lifting of L-Narrowing Derivations

Abstract

If conditional rewrite/rules are restricted to the form  ... where P is a finite set of equations, f is any function symbol, x1, …, xn are variables, and t is any term when the premise P contains in general variables which do not occur in the list x1, …, xn. 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-narrowing, closely related to lay-narrowing. Two lifting lemmas are shown which characterize the relationship of L/narrowing derivations if the goals are modified by substitutions. From these lifting lemmas, soundness and completeness results can be concluded.