The declarative semantics of the Prolog selection rule

We axiomatize the Prolog selection rule which always selects the leftmost literal in a goal. We introduce a new completion of a logic program which we call the l-completion of the program. The l-completion is formulated as a first-order theory in a language extended by new predicate symbols which express success, failure and left-termination of queries. The main results of the paper are the following. If a query succeeds, fails or is left-terminating under the Prolog selection rule, then the corresponding formula in the extended language is provable from the l-completion. Conversely, if a logic program and a query are correct with respect to some mode assignment and if one can prove in the l-completion that the query succeeds and is left-terminating, then the goal is successful and Prolog, using its depth first search, will compute an answer substitution for the goal. This result can even be extended to so called non-floundering queries