We cope with the problem of correctness and optimality for logic
programs analysis by abstract interpretation.  We refine the
goal-dependent framework appeared in [CF99] by fixing a result
of correctness and introducing two specialized operators for forward
and backward unification. We provide the best correct abstractions
of the concrete operators in the case of set-sharing analysis.  We
show that the precision of the overall analysis is strictly improved
and that, in some cases, we gain precision w.r.t. more complex
domains involving linearity and freeness information.