# unification index

It is an data index to retrieve among a set of terms (or atoms) the ones which unify with an input term (or atom). In the case, it is called an *exact unification index*, otherwise it may only filter candidates for unification.

## Resources

- DBLP:phd/de/Motik2006 contains a paragraph about unification indexing in description logics
- coordinate-indexing method (also called FPA indexing) is explained in the path indexing report, is an exact unification index, if the terms do not contain several times the same variable.
- path indexing is a refinement of coordinate-indexing and describes terms by a mapping from paths to symbols, e.g. Symbol(f(a,g(x,y)), <f,2,g,1>) = x