Control Generation for Logic Programs

A basic requirement of declarative programming is to free the program-mer from the need to manually insert control annotations into the program. Here we study the execution of logic programs under coroutining computa-tion 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 termi-nation 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 out-put 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 Plümer.