We advocate using the declarative reading in proving partial correctness of logic programs, when the properties of interest are declarative. Some recently published work presents unnecessarily complicated methods for proving such properties. These approaches refer to the operational semantics, as they consider calls and successes of the predicates of the program during LD-resolution. We show that this is an unnecessary complication and that a straightforward proof method is simpler and more general. Our approach is based solely on the property that ``whatever is computed is a logical consequence of the program''. This approach is not new and can be traced back to the work of Clark in 1979. However it seems that it has been - to a certain extent - forgotten. The paper deals with partial correctness, we complement it with an outline of a method for proving completeness.