Termination of Logic Programs with block Declarations Running in Several Modes

Smaus, J.G. and Hill, P.M. and King, A. (1998) Termination of Logic Programs with block Declarations Running in Several Modes. In: Palamidessi, C., ed. Proceedings of the 10th International Symposium on Principles of Declarative Programming. Lecture Notes in Computer Science, 1490. Springer-Verlag, see also http://www.springer.de/comp/lncs/index.html pp. 73-88. ISBN 3-540-65012-1 .

PDF
Download (248Kb)	Preview
Postscript
Download (219Kb)	Preview

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.

Item Type:	Conference or workshop item (Paper)
Uncontrolled keywords:	Logic programming, coroutining, delay declarations, block declarations, termination, modes, selection rules
Subjects:	Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions:	Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Depositing User:	Mark Wheadon
Date Deposited:	22 Aug 2009 15:16
Last Modified:	25 Jun 2012 10:14
Resource URI:	http://kar.kent.ac.uk/id/eprint/21647 (The current URI for this page, for reference purposes)

• Depositors only (login required):