Many Prolog systems search for solutions by using a fixed rule to choose an atom to carry out a derivation step. This approach is not always adequate, since termination cannot be guaranteed, even if the program under consideration has a solution. Dynamic scheduling is concerned with the issue of choosing the atom to be selected at runtime, without using a fixed selection rule. In order to model and analyze this topic, the class of input consuming derivations is introduced and analyzed.

This paper is concerned with two central topics: the semantics of partial derivations, and the termination of these derivations. While the first topic is modeled by defining a slight modified immediate consequence operator, the termination criterion derived here relies on several techniques, such as input terminating programs (programs that only produce finite input consuming derivations, given certain queries as inputs) and level mappings. The key result is that the property of being simply acceptable is a sufficient and necessary criterion for input termination.

The paper is written formally, and is clear and easily readable. What is most important, in my opinion, is that the authors have included many illustrative examples, which make the key concepts clear. For example, the Quicksort example from section 5.2 is more than one page long, and explains everything in detail. Another section (section 6) is devoted to additional examples demonstrating the usefulness of the concepts described in the text.