Jahama, SaidKfoury, A.J.2011-09-122011-09-121993-12-20Jahama, Said; Kfoury, A.J.. "A General Theory of Semi-Unification", Technical Report BUCS-1993-018, Computer Science Department, Boston University, November 1993. [Available from: http://hdl.handle.net/2144/1476]https://hdl.handle.net/2144/1476Various restrictions on the terms allowed for substitution give rise to different cases of semi-unification. Semi-unification on finite and regular terms has already been considered in the literature. We introduce a general case of semi-unification where substitutions are allowed on non-regular terms, and we prove the equivalence of this general case to a well-known undecidable data base dependency problem, thus establishing the undecidability of general semi-unification. We present a unified way of looking at the various problems of semi-unification. We give some properties that are common to all the cases of semi-unification. We also the principality property and the solution set for those problems. We prove that semi-unification on general terms has the principality property. Finally, we present a recursive inseparability result between semi-unification on regular terms and semi-unification on general terms.en-USTechnical Report