Errata

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].

Also, a reference is missing to the paper of Malfon [1994], which generalizes to normal programs the proof method for completeness of Deransart and Małuszyński, discussed here in Section 5.3. The approach of Malfon deals with the well-founded semantics, the Fitting semantics and a semantics close to the Kunen semantics.

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.
Malfon, B. 1994. Characterization of some semantics for logic programs with negation and application to program validation. Proceedings of the 1994 International Logic Programming Symposium, 91-105.