Is the reification the same or similar as the unification of a logical variable? The "The common portion defines logic variables, constraint states, unification, and reification" (First-order miniKanren representation: Great for tooling and search_) suggests they're not the same._ I guess that unification is binding a logical variable to concrete value, while reification is binding it to a value like _0, which shows it can take any value.