Lifting of L-Narrowing Derivations

Authors

  • P. Bachmann

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.

Downloads

Download data is not yet available.

How to Cite

Bachmann, P. (2012). Lifting of L-Narrowing Derivations. COMPUTING AND INFORMATICS, 16(3), 309–334. Retrieved from https://www.cai.sk/ojs/index.php/cai/article/view/662