| What makes Prolog, Prolog is not unification on its own but SLD-Resolution with unification, where "SLD" stands for [L]inear Resolution with a [S]election rule restricted to [D]efinite clauses. If you know your Resolution typology, that means soundness and refutation-completeness (or completeness with subsumption) [1]. I don't think I've ever seen a discussion of Resolution in functional programming textbook implementations of "Prolog". They typically just bodge some depth-first search with backtracking and unification in polish notation and call it "Prolog", or "logic programming". A bit like if I wrote a "lisp" with eval(X):- call(X), then completely ignored all that jazz about lambda calculus and concentrated on garbage collection and linked lists. A good starting point instead, if one wishes to understand Prolog and not just dismiss it out of hand, is to try and understand Resolution, and what unification does for Resolution, and why it ended up in Prolog (and how) in the first place. I'd start, well, at the beginning: A Machine-Oriented Logic Based on the Resolution Principle https://www.semanticscholar.org/paper/A-Machine-Oriented-Log... Where you can follow the progress from ground Resolution, to unification, the Resolution theorem, and all the way to the (pre-modern) Subsumption Theorem. It's a long way to Prolog from there, but that's where it all begins. _______________ [1] Although Prolog implemented by DFS is not complete if Prolog implemented by DFS is not complete (etc). |