Technical Report No. 203 - Abstract

Jan-Georg Smaus
Termination of Logic Programs Using Various Dynamic Selection Rules

We study termination of logic programs with dynamic sched­uling, 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, for example being ground in the input positions. In another dimension, we consider both local and non-local derivations. In all cases, we give sufficient and necessary criteria for termination. The dimensions can freely be combined, yielding the most comprehensive approach so far to termination of logic programs with dynamic scheduling.