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.
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.