Loop checking in SLD-derivations by well-quasi-ordering of goals