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 un-fold/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 pair-wise disjoint vectors of variables, the unfold/fold proof method can be used to show that the equivalence formula ∀X (∃Y F (X,Y) ↔ ∃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 seman-tics if we find non-ascending unfold/fold proofs of the corresponding equiva-lence 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