Bounded nondeterminism of logic programs

The notion of bounded nondeterminism for logic programs and queries is introduced. A program and a query have bounded nondeterminism iff there are finitely many refutations for them via any selection rule. We offer a declarative characterization of the class of programs and queries that have bounded nondeterminism by introducing bounded programs and queries. A direct application of the theoretical framework is concerned with the automatic generation of a terminating control for a given program and query. We provide a simple transformational approach that, under the assumption of boundedness, ensures strong termination of the transformed programs and queries, while preserving refutations. Also, we outline an adaptation of an automatic termination method to the purpose of inferring boundedness.