On logic programs that do not fail

This paper investigates the advantages of reasoning on logic programs and queries that have only successful derivations. We consider an extension of the logic programming paradigm that combines guarded clauses and delay declarations. The main contribution of this paper consists of some general conditions for a class of programs and queries which imply that successful derivations only are present. A few practical instances of the method are studied, and their applicability demonstrated. The general conditions are derived extending proof methods originally developed for Prolog's programs. From the point of view of parallelism, the method is able to reason about termination (with success) of pipeline parallel executions of programs. In particular, we show some examples of parallelization of terminating Prolog programs. Moreover, from the point of view of nondeterminism, don't care nondeterminism can be safely adopted for the class of programs that have only successfull derivations.