Robinson’s algorithm unifies first-order terms by solving their equations. It gradually constructs a substitution that fills holes, or detects a contradiction proving that no solution exists. section 10.7
Its central checks are:
- Build substitutions incrementally as equations between binary terms are resolved. section 10.7
- Allow holes to alias other holes, preserving shared unknowns in the solution. section 10.7
- Run an occurs check before substituting, rejecting a hole mapped to a term containing itself and preventing infinite recursion. section 10.7
Where it is used
Unification supports compiler type inference and related logical deductions. Combined with backtracking search, it can solve general first-order logic problems, as in Prolog. section 10.7
