It can be useful to tackle unification in two steps, even in Prolog. By pattern-matching first (a la functional programming) we quickly get either a failure or a set of
distinct variables with constraints, which the second 'proper unification' step can try to solve.
For example, unifying `plus(1, 2)` with `plus(X, X)` can start by pattern-matching, which turns the latter into `plus(X, Y)` with the constraint X = Y (to avoid variables occuring more than once). The match will succeed, producing the constraints X = 1 and Y = 2, along with the X = Y constraint from before. The second step will try to solve these constraints, and fail since they're inconsistent.
I've not done much logic programming, but I've encountered this two-step approach as a way to implement co-inductive logic programming, which lets us handle infinite datastructures like streams.
