UNIFICATION IN INCOMPLETELY SPECIFIED THEORIES - A CASE-STUDY

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.