Unfold/fold transformations have been studied for a number of years. They were initially applied to functional programs, and, later, in the work of Tamaki and Sato, to logic programs, which is the area of concern of this paper.

Basically, unfolding is the act of replacing an instantiation of the head of a clause by the instantiation of the body of the clause, and folding is the act of replacing an occurrence of the body by the head of a clause. Unfolding preserves correctness (same least Herbrand model), but folding ensures only partial correctness.

The paper introduces a general approach to constructing transformation systems in which folding is totally correct. To this end, a parameterized transformation framework is described. This makes use of a measure structure to maintain the bookkeeping of the transformations. The measure structure contains a well-founded order, so that an induction relative to this order relation can be used to prove the total correctness of folding. Selecting different measure structures will lead to different transformation systems. In particular, it is shown how the well-known systems of Tamaki and Sato, and also Kanamori and Fujita, fit into this framework.

The transformation framework is also augmented to permit goal replacement as a valid operation. Goal replacement allows semantically equivalent conjunctions to be interchanged.

As well as producing the two transformation systems already mentioned, by instantiating the framework, the authors produce a new system called SCOUT, which supports disjunctive folding on recursive clauses and subsumes the other systems. An application of SCOUT has been used to construct inductive proofs of temporal properties of concurrent systems. To automate the goal replacement rule, a syntactic version the rule is introduced (since proving the semantic equivalence of goals is, in general, undecidable).

The introduction of the parameterized framework provides a uniform approach to constructing transformation systems, and allows different systems to be compared. This is a valuable addition to the work on transformation systems.