@article{oai:nagoya.repo.nii.ac.jp:00007556,
 author = {Nishida, Naoki and Sakai, Masahiko and Sakabe, Toshiki},
 journal = {12th International Workshop on Functional and (Constraint) Logic Programming},
 month = {Jun},
 note = {Term rewriting systems (TRSs) are extended by allowing to contain extra variables in their rewrite rules. We call the extended systems EV-TRSs. They are ill-natured since every one-step reduction by their rules with extra variables is infinitely branching and they are not terminating. To solve these problems, this paper extends narrowing on TRSs into that on EV-TRSs and show that it simulates the reduction sequences of EV-TRSs as the narrowing sequences starting from ground terms. We prove the soundness of ground narrowing-sequences for the reduction sequences. We prove the completeness for the case of right-linear systems, and also for the case that no redex in terms substituted for extra variables is reduced in the reduction sequences. Moreover, we give a method to prove the termination of the simulation, extending the termination proof of TRSs using dependency pairs, to that of narrowing on EV-TRSs starting from ground terms.},
 pages = {198--211},
 title = {Narrowing-based Simulation of Term Rewriting Systems with Extra Variables and its Termination Proof},
 year = {2003}
}