Termination of Logic Programs Using Various Dynamic Selection Rules
Abstract
We study termination of logic programs with dynamic scheduling, as it
can be realised using delay declarations. Following previous work, our
minimum assumption is that derivations are input-consuming, a
notion introduced to define dynamic scheduling in an abstract
way. Since this minimum assumption is sometimes insufficient to ensure
termination, we consider here various additional assumptions on
the permissible derivations. In one dimension, 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. In all cases,
we give sufficient criteria for termination. The dimensions can be
combined, yielding the most comprehensive approach so far to
termination of logic programs with dynamic scheduling. For non-local
derivations, the termination criterion is even necessary.
Jan-Georg Smaus
Last modified: Wed Sep 15 13:15:58 MEST 2004