In logic programming, dynamic scheduling is a general term for a situation where the selection of the atom in each resolution (computation) step is determined at runtime, as opposed to a fixed selection rule such as the usual left-to-right selection rule of Prolog. This has applications e.g. in parallel programming or in implementing the test-and-generate paradigm. A mechanism to control dynamic scheduling is provided in existing languages in the form of delay declarations.
Input-consuming derivations were introduced to describe dynamic scheduling while abstracting from the technical details. In this paper, we first formalize the relationship between delay declarations and input-consuming derivations, showing that, in many cases, a one-to-one correspondence holds. Then, we define a model-theoretic semantics for input-consuming derivations of simply-moded programs and queries. Finally, for this class of programs, we provide a necessary and sufficient criterion for termination of input-consuming derivations.