Most widely used logic program transformation systems are based on the unfold/fold transformation technique that was introduced Burstall&Darlington for functional programming and was adapted for logic programming by Tamaki&Sato. Since then, many works have been devoted to study logic program transformations based on the unfold/fold technique.

Unfold/fold transformation systems strongly depend on the considered semantics. Some of the most used semantics are well-founded semantics, perfect model semantics, computed answer set semantics or program
completion related semantics.

In general, there are no significant differences in the rule unfolding, since unfolding is correct w.r.t. most of the considered semantics. However, the treatment of the rule folding is more intricate than the one of the unfolding rule and, besides, it depends on the considered semantics and differs from one approach to other. Among the works that consider completion related semantics, there are two main approaches. On one hand, Tamaki&Sato-style systems split predicates into two sets ---old and new predicates---, restricting the application of rules according to this partition. These systems usually assume that programs are given once and for all. Hence, given a sequence of programs that have been obtained by transformation, the clauses in the last program are transformed using the clauses in the initial program. Another feature of Tamaki&Sato-style systems is that they usually require that the folded literals come from an unfolding step in order to ensure the correctness of folding transformations. On the other hand, there exist some systems that do not partition predicates, but folding transformations can only use clauses in the last program of the transformation sequence as folder clauses. Therefore, these transformation systems are often less powerful than Tamaki&Sato-style systems.