A most general unifier is a unifying substitution through which every other unifier factors by a further substitution. It records exactly the equality constraints forced by the terms.

Articles by others on the same topic (0)

There are currently no matching articles.