@michelemendel Not sure where that statement comes from, but your interpretation sounds about right. Unification is really just the process of making both sides of the equality operation equivalent, by bidirectionally binding the variables etc… I think reification means just lifting logic variables into the language as first order concepts. They’re made real in that not only are they symbols in your program, but you can also pass them around as values.

Actually scratch that, I think you’re right about reification in this context.

Good, then I know my understanding is correct. It's interesting to note how all the tutorials and academic papers take for granted that a certain terminology should somehow be obvious and known to all.

yeah, there is a deep assumption in core.logic that you've read the reasoned schemer (which I have not), which makes making sense of the soup of protocols very tricky. I've been fiddling with adding clp(set) (reasoning over sets, having goals fir things like set unions, etc) to core.logic, and sort of releated to the previous discussion similar to how core.logic adds lcons for lists that aren't completely specified, I need to add a new logic set type for sets that aren't completely known. For interops sake I would like to, at the very end before reporting results, replace any logic sets that are fully specified with real clojure sets, and I think core.logics IReifyTerm protocol is the way to do that, but so far I haven't gotten it to work (if you introduce a clojure set in the wrong place something in core.logic goes nuts and blows the stack)