Proofs of declarative properties of logic programs

Abstract

In this paper we shall consider proofs of declarative properties of Logic Programs, i.e. properties associated with the logical semantics of pure Logic Programs, in particular what is called the partial correctness of a logic program with respect to a specification. A specification consists of a logical formula associated with each predicate and establishing a relation between its arguments. A definite clause program is partially correct iff every possible answer substitution satisfies the specification. This paper generalizes known results in logic programming in two ways: first it considers any kind of specification, second its results can be applied to extensions of logic programming such as functions or constraints. In this paper we present two proof methods adapted from the Attribute Grammar field to the field of Logic Programming. Both are proven sound and complete. The first one consists of defining a specification stronger than the original one, which furthermore is inductive (fix-point induction). The second method is a refinement of the first one: with every predicate, we associate a finite set of formulas (we call this an annotation), together with implications between formulas. The proofs become more modular and tractable, but the user has to verify the consistency of his proof, which is a decidable property. This method is particularly suitable for proving the validity of specifications which are not inductive.