Lifting of L-Narrowing Derivations
P. Bachmann
Computing and Informatics, Tome 28 (2012) no. 1, / Harvested from Computing and Informatics
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.
Publié le : 2012-01-26
Classification: 
@article{cai662,
     author = {P. Bachmann},
     title = {Lifting of L-Narrowing Derivations},
     journal = {Computing and Informatics},
     volume = {28},
     number = {1},
     year = {2012},
     language = {en},
     url = {http://dml.mathdoc.fr/item/cai662}
}
P. Bachmann. Lifting of L-Narrowing Derivations. Computing and Informatics, Tome 28 (2012) no. 1, . http://gdmltest.u-ga.fr/item/cai662/