Completeness of Extended Unification Based on Basic Narrowing
Akihiro Yamamoto, 章博 山本 · Institutional Repositories DataBase (IRDB) · 1988
In this paper we prove the completeness of unification based on the basic narrowing. first we prove the completeness of unification based on original narrowing under a weaker condition than the previous proof. Then we discuss the relation between basic narrowing and innermost reduction as the lifting lemma, and prove the completeness of unification based on the basic narrowing. Moreover, we give the switching lemma to combine the previous algorithm and our new proof.