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, in the style of concurrent logic languages, and dynamic selection rules. Some general conditions for a class of programs and queries are stated, which characterize when successful derivations only are present. A few practical instances of the general conditions are studied, and their applicability to real programs demonstrated. The main contributions of the proposed method are: (i) don't care non determinism can be safely adopted for programs that do not fail, (ii) termination of process networks expressed as logic programs can be proved, by means of a simple proof method developed for a fixed selection rule, and (iii) a strategy for parallelizing terminating Prolog programs is identified.