Not that I've seen yet, but the manual does include this passage:

> Strand provides pattern matching but no general unification, instead logic variables must be explicitly assigned, which simplifies the semantics considerably.

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.