Proof method of partial correctness and weak completeness for normal logic programs

AbstractWe present a proof method for partial correctness and weak completeness for any normal programs, which coincides with the already known proof methods for partial correctness and completeness for definite programs. The purpose of such a validation method is to compare the actual semantics of a program with some expected properties, sometimes called specifications. We consider that the actual semantics of a normal program is the three-valued well-founded semantics. Thus the actual semantics of a program is defined by two sets of ground atoms: the set of the true atoms and the set of the false atoms.The expected properties may be formulated also by two sets of ground atoms; partial correctness and weak completeness are formulated by set inclusions.Soundness and completeness of our proof method comes from an inductive characterization of the well-founded model.The method may be used also to prove that some given set of atoms characterizes exactly the set of true atoms, if the semantics is in fact bivalued and the specification is total