  Logic program transformation by the unfold/fold method ad- vocates the
writing of correct logic programs via the application of some rules to a naive
program. This work focuses on how to overcome subgoal- introduction
difficulties in synthesizing efficient sorting algorithms from an naive sorting
algorithm, through logic program transformation and abductive reasoning.
