to W. Drabent. Correctness and Completeness of Logic Programs. ACM Transactions on Computational Logic. 17, 3, Article 18 (May 2016), 32 pages. DOI: 10.1145/2898434.

In "Related Work", a reference is missing to the annotation method of Deransart for proving program correctness [Deransart and Małuszyński 1993, Deransart 1993, Boye and Małuszyński 1997]. As briefly described in [Drabent and Miłkowska 2005, Section 5]:

An approach related to ours is the annotation method of Deransart [Deransart 1993, section 4; Boye and Małuszyński 1997, section 4] for proving definite program correctness. It can be seen as refinement of the natural method of section 3.1, where one proves more (but smaller) implications than those to be proved in the natural method.
Here "natural method" stands for the method of Theorem 4.1 by Clark [1979]. It is worth adding that the attribution of the method to Clark is due to Deransart [1993].

References not present in the article

Deransart, P. 1993. Proof methods of declarative properties of definite programs. Theoretical Computer Science 118, 99–166.
Boye, J. and Małuszyński, J. 1997. Directional types and the annotation method. Journal of Logic Programming 33, 3, 179–220.