Control generation for logic programs

A basic requirement of declarative programming is to free the programmer from the need to manually insert control annotations into the program. Here we study the execution of logic programs under coroutining computation rules. We define a new systematic approach to when-declarations; we introduce a class of simple, yet powerful, instantiation based computation rules which are particularly easy to manipulate and to relate with the termination of SLD-derivations. The task is then, given a logic program, to find a computation rule which allows an efficient and terminating execution of goals. We present an algorithm scheme to generate such computation rules by stepwise refinement and simulated execution. We discuss the scheme as well as a concrete algorithm and its results. The algorithm yields useful output for a relevant class of programs, including guaranteed termination for most of the programs discussed in the work on termination by Apt et. al., Bruynooghe et. al., and Plumer.