All true, but I stand by my assertion (pardon the pun) that "Prolog SLD resolution" is depth first -- unless you're using a non-standard Prolog or some meta-predicate that implements another strategy. And any other strategy that's not WAM-inspired and depth first is prohibitive and unwarranted for the actual running of Prolog programs with all its assumed operational semantics. General resolution (SLD or otherwise) works for some theorem-proving, but not for running general Prolog programs.
Hey. If you are still reading this, I must apologise for my other sibling comment right under yours. I sound like a formalism nazi! I understand what you mean that "Prolog SLD resolution is depth first". You have probably implemented a Prolog meta-interpreter and noticed that it works by putting literals on the stack, then deriving new literals and putting those on the stack, recursively and by creating a new "branch" between each literal. In fact, resolution itself is often described (or rather reasoned about) in terms of resolution trees. It's definitely not the same as depth first search, because it's not a search, but it doesn't take a lot of effort to see what you mean by "depth first" in this case. I should not have been such a terminology miser here. I'm upset myself sometimes when people demand absolute terminological clarify of me when it's obvious what I'm trying to say (and it's obvious to them, they just like to nitpick). So I apologise for the nitpicking.
Your original comment said that "default Prolog SLD resolution is just a depth-first search". SLD resolution is not "depth-first search", "just" or with additions. Depth-first search is a search algorithm. In Prolog, depth-first search is used to find literals that unify with a goal, in order to perform resolution. But depth-first search is not part of SLD resolution and depth-first search and SLD resolution are not the same algorithm.
You seem to be reformulating your assertion. In the last comment you say that "default Prolog SLD resolution is depth-first". That reformulation also doesn't make sense. The search used by Prolog is depth-first search. But SLD resolution is not "depth-first". There is no context in which "depth-first" makes sense outside of depth-first search and there is no context in which SLD resolution can be said to be "depth-first". That's regardless of implementation.
>> General resolution (SLD or otherwise) works for some theorem-proving, but not for running general Prolog programs.
I'm sorry, I don't understand this. If I understand correctly, "general" resolution refers to resolution for arbitrary clauses? SLD resolution operates on definite clauses and is sound and refutation complete for definite logic programs. SLDNF resolution is also sound for normal programs. So, yes, resolution "works" for running general Prolog programs.
