**Dept. of Computer and Information science, Linköping University**

## IDA Technical Reports: abstract

*Generated: Mon, 04 May 2015 02:57:38 *

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.

**Goto (at Linköping University):**
```
CS Dept
TR Overview
```

*<webmaster@ida.liu.se>*