First-order unification seeks substitutions making first-order terms identical. Constructor decomposition and the occurs check produce a most general unifier when one exists.
Articles by others on the same topic
There are currently no matching articles.