On logic programs that always succeed

AbstractWe introduce a generalized definition of SLD-resolution admitting restrictions on atom and/or clause selectability. Instances of these restrictions include delay declarations, input-consuming unification and guarded clauses.In the context of such a generalization of SLD-resolution, we offer a theoretical framework to reason about programs and queries such that all derivations are successful. We provide a characterization of those programs and queries which allows to reuse existing methods from the literature on termination and verification of Prolog programs