@techreport{R-90-11, TITLE = {Unification in Classes of Equational Theories: A Case Study}, AUTHOR = {Staffan Bonnier}, YEAR = {1990}, NUMBER = {R-90-11}, INSTITUTION = ida, ADDRESS = idaaddr, ABSTRACTURL = {/publications/cgi-bin/tr-fetch.pl?r-90-11+abstr}, ABSTRACT = {Let T be an equational theory and let P be a unification procedure. In order to initiate P to do unification in T, T must in some way be presented to P. Due to practical considerations, P can sometimes only obtain approximations of T: Each approximation specifies a class of theories in which T is just a single member. In this paper it is suggested to use approximation frames to formally characterize these classes. As a consequence, each approximation frame also specifies which complete sets of T-unifiers that are strongly complete. Those are the only complete sets of T-unifiers that can be found within the scope of accessing only available approximations of T. A unification procedure which finds such sets whenever they exist is said to be weakly complete. These concepts are specialized to the study of so called evaluation based unification algorithms: An approximation frame characterizing the inherent incompleteness of such algorithms is given. Finally a weakly complete evaluation based algorithm is developed. }, IDANR = {LiTH-IDA-R-90-11}