Deriving sorting algorithms via abductive logic program transformation

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.