Bonnier, S. (1990). Unification in Classes of Equational Theories: A Case Study. Technical Report LiTH-IDA-R-90-11, Department of Computer and Information Science, Linköping University, Sweden. (bibtex),
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.
CS Dept TR Overview