The evaluation of a goal for a logic program can be viewed as the search for an answer, written in the constraints language, that correctly implies the goal. We propose a small set of inference rules, correct w.r.t. the completion of a program and the Clark equational theory, which is strong enough to compute a complete set of answers for extended programs over the Herbrand constraint system. The basic step, the unfolding, is shown to realize, in a syntactic way, the inverse of what Fitting's functional computes in the semantic one. Then, using the fundamental result of Kunen, we can prove the completeness of our schema for the three valued consequences of the completion.