Bounded Nondeterminism of Logic Programs

We introduce the notion of bounded nondeterminism for logic programs and queries. A program and a query have bounded nondeterminism if 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 defining bounded programs and queries. The characterization is provided in terms of Herbrand interpretations and level mappings, in the style of existing characterizations of universal termination. A direct application of the theoretical framework is concerned with the automatic generation of a terminating control. We present a transformational approach that given a bounded program and a bounded query yields a terminating program and query with the same set of refutations. Concerning the issue of automating the approach, by means of an example we sketch how an automatic method for proving left termination can be adapted to the purpose of inferring boundedness. Such an ad...

• Type: Conference
• Year: 1999
• Where: ICLP
• Authors: Dino Pedreschi, Salvatore Ruggieri
• Keywords: Automated Reasoning, Characterizations, Declarative Characterization, ICLP 1999, Logic Programs