It is declarative on reasoning about logic programs
Włodzimierz Drabent · 1999
We advocate using the declarative reading of logic programs in proving partial correctness, when the properties of interest are declarative. Some publications present 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 in some sense 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. We believe in its importance in teaching logic programming. The paper deals with partial correctness, we complement it with an outline of a method for proving completeness. In this paper we recall a simple and straightf...