© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Termination of Logic Programs with block Declarations Running in Several Modes
Jan-Georg Smaus, Pat Hill, and Andy King
In Catuscia Palamidessi, editor, International Symposium on Programming Languages: Implementations, Logics and Programs, jointly held with Algebraic and Logic Programming, volume 1490 of Lecture Notes in Computer Science, pages 182-196. Springer-Verlag, see also http://www.springer.de/comp/lncs/index.html, June 1998.Abstract
We show how termination of logic programs with delay declarations can be proven. Three features are distinctive of this work: (a) we assume that predicates can be used in several modes; (b) we show that block declarations, which are a very simple delay construct, are sufficient; (c) we take the selection rule into account, assuming it to be as in most Prolog implementations. Our method is based on identifying the so-called robust predicates, for which the textual position of an atom using this predicate is irrelevant. The method can be used to verify existing programs, and to assist in writing new programs. As a byproduct, we also show how programs can be proven to be free from occur-check and floundering.
Download publication 219 kbytes (PostScript)
Bibtex Record
@inproceedings{590,
author = {Jan-Georg Smaus and Pat Hill and Andy King},
title = {{Termination of Logic Programs with block Declarations Running in Several Modes}},
month = {June},
year = {1998},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1998/590},
booktitle = {International Symposium on Programming Languages: Implementations, Logics and Programs, jointly held with Algebraic and Logic Programming},
editor = {Catuscia Palamidessi},
publisher = {Springer-Verlag, see also http://www.springer.de/comp/lncs/index.html},
refereed = {yes},
series = {Lecture Notes in Computer Science},
volume = {1490},
}