First-order unification 2026-10-20
View more
First-order unification seeks substitutions making first-order terms identical. Constructor decomposition and the occurs check produce a most general unifier when one exists.
Read the full article