As has been pointed out in many of the already published research works, the hyperresolution refinements-based decision procedures have proved appropriate in case of a large class of decidable classes of clause sets. The research reported in the present paper proposes a fully algorithmical method for the construction of models out of termination sets of positive hyperresolution provers. Moreover, a formal framework for model building by resolution based on resolution operators and orthogonalization is developed, essentially based on the finite atomic representation of a Herbrand model. It is argued that the atomic representations are suitable and prove their usefulness as model descriptions, by showing that it is decidable whether two given atomic representations are equivalent and that arbitrary clauses can effectively be evaluated with respect to the represented models. Following to a series of preliminary results exposed in the first two sections, the hyperresolution as decision procedure is presented in the third section. The problem of representing Herbrand models and the construction of equivalent atomic representations are developed in the next three sections. It is showed that \(H\)-assumption is of crucial value for an algorithmic evaluation of clauses and several results concerning the problem of extracting finite models. A series of comments, suggestions for further research work and concluding remarks are formulated in the final section of the paper.