Logic in Computer Science (LICS 1994)

Paper: The declarative semantics of the Prolog selection rule (at LICS 1994)

Authors: Robert Stark

Abstract

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

BibTeX

  @InProceedings{Stark-Thedeclarativeseman,
    author = 	 {Robert Stark},
    title = 	 {The declarative semantics of the Prolog selection rule},
    booktitle =  {Proceedings of the Ninth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1994},
    year =	 1994,
    editor =	 {Samson Abramsky},
    month =	 {July}, 
    pages =      {252--261},
    location =   {Paris, France}, 
    publisher =	 {IEEE Computer Society Press}
  }