Synthesis and Transformation of Logic Programs Using Unfold/Fold Proofs

We present a method for proving properties of definite logic programs. This method is called unfold/fold proof method because it is based on the unfold/fold transformation rules. Given a program P and two goals (that is, conjunctions of atoms) F(X,Y ) and G(X,Z), where X, Y , and Z are pairwise disjoint vectors of variables, the unfold/fold proof method can be used to show that the equivalence formula Exists X (Exists Y F(X,Y ) <-> Exists Z G(X,Z)) holds in the least Herbrand model of P. Equivalence formulas of that form can be used to justify goal replacement steps, which allow us to transform logic programs by replacing old goals, such as F(X,Y ), by equivalent new goals, such as G(X,Z). These goal replacements preserve the least Herbrand model semantics if we find non-ascending unfold/fold proofs of the corresponding equivalence formulas, that is, unfold/fold proofs which ensure suitable well-founded orderings between the successful SLD derivations of F(X,Y ) and G(X,Z), respectively.