Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Ninth Annual IEEE Symposium on

Logic in Computer Science (LICS 1994)

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

Authors: Robert F. Stärk

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{Strk-Thedeclarativeseman,
    author = 	 {Robert F. Stärk},
    title = 	 {The declarative semantics of the Prolog selection rule},
    booktitle =  {Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS 1994)},
    year =	 {1994},
    month =	 {July}, 
    pages =      {252--261},
    location =   {Paris, France}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski