In the context of abstract interpretation based static analysis, we
cope with the problem of correctness and optimality for logic program
analysis. We propose a new framework equipped with a denotational,
goal-dependent semantics which refines many goal-driven frameworks
appeared in the literature. The key point is the introduction of two
specialized concrete operators for forward and backward unification.
We prove that our goal-dependent semantics is correct w.r.t. computed
answers and we provide the best correct approximations of all the
operators involved in the semantics for 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.