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