Some Relationships between Unification, Restricted Unification, and Matching

Abstract

We present restricted T-unification that is unification of terms under a given equational theory T with the restriction that not all variables are allowed to be substituted. Some relationships between restricted T-unification, unrestricted T-unification and T-matching (one-sided T-unification) are established. Our main result is that, in the case of an almost collapse free equational theory the most general restricted unifiers and for certain termpairs the most general matchers are also most general unrestricted unifiers, this does not hold for more general theories. Almost collapse free theories are theories, where only terms starting with projection symbols may collapse (Le to be T-equal) to variables.