Termination of Logic Programs for Various Dynamic Selection Rules
Abstract
We study termination of logic programs with dynamic scheduling, as
it can be realised using delay declarations. Our minimum assumption
is that derivations are input-consuming, a notion introduced to
define dynamic scheduling in an abstract way. We then give
sufficient criteria for termination under various additional
assumptions. We consider derivations parametrised by any property
that the selected atoms must have, e.g. being ground in the input
positions. In another dimension, we consider both local and
non-local derivations. These dimensions can freely be combined,
yielding the most comprehensive approach so far to termination of
logic programs with dynamic scheduling.