It might partially have been inspired by Prolog, in fact. But it lacks backtracking and unification so I don't think it qualifies as an embedded Prolog system. Erlang allows so-called non-linear patterns (ie using the same variable for several argument positions, implying equality), which comes slightly closer to Prolog (and of course, Erlang was originally modeled on Prolog, but the apple ended up far from the tree).

At compile-time, sure. But ML-like languages in general have no support for runtime logical programming. They don't provide an API to do things like type inference at runtime. For a good reason too, the only possible way type inference in ML-like languages work is because the computational cost is abstracted away from the runtime. Logical programming (ala Prolog) is very useful but the truth is it's asymptotically inefficient. Standard ML's type inference algorithm was, for example, asymptotically exponential. It just so happened that for useful programs it halts in a reasonable amount of time. This is not something you can provide an API for so that at runtime you can run arbitrary type inferences.