We show the completeness of an extension of 
SLD--resolution to the equational setting.  
This proves a conjecture of Laurent Fribourg and
shows the completeness of an implementation of his.  
It is the first completeness result for superposition 
of equational horn clauses which reduces to SLD 
resolution in the non--equational case.  The inference 
system proved complete is actually more general than 
the one of Fribourg, because it allows for a selection 
rule on program clauses.  Our completeness result also 
has implications for Conditional Narrowing and Basic 
Conditional Narrowing.