Controlling Conjunctive Partial Deduction

Partial deduction within Lloyd and Shepherdson's framework transforms different atoms of a goal independently and therefore fails to achieve a number of unfold/fold transformations. A recent framework for conjunctive partial deduction allows unfold/fold transformations by specialisation of entire conjunctions, but does not give an actual algorithm for conjunctive partial deduction, and in particular does not address control issues (e.g. how to select atoms for unfolding). Focusing on novel challenges specific to local and global control, we describe a generic algorithm for conjunctive partial deduction, refine it into a fully automatic concrete algorithm, and prove termination and correctness