School of Computing

Preventing Instantiation Errors and Loops for Logic Programs with Multiple Modes Using block Declarations

Jan-Georg Smaus, Pat Hill, and Andy King

In P Flener, editor, Logic Programming, Synthesis and Transformation (Selected Papers), volume 1559 of Lecture Notes in Computer Science, pages 182-196. Springer-Verlag, March 1999 Copyright Springer-Verlag, see http://www.springer.de./comp/lncs/index.html.

Abstract

This paper presents several verification methods for logic programs with delay declarations. It is shown how type and instantiation errors related to built-ins can be prevented, and how termination can be ensured. Three features are distinctive of this work: it is assumed that predicates can be used in several modes; it is shown that block declarations, which are a very simple delay construct, are sufficient to ensure the desired properties; the selection rule is taken into account, assuming it to be the rule of most Prolog implementations. The methods can be used both to verify existing programs and to assist in writing new programs.

Download publication 231 kbytes (PostScript)

Bibtex Record

@inproceedings{682,
author = {Jan-Georg Smaus and Pat Hill and Andy King},
title = {{Preventing Instantiation Errors and Loops for Logic Programs with Multiple Modes Using block Declarations}},
month = {March},
year = {1999},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {Copyright Springer-Verlag, see http://www.springer.de./comp/lncs/index.html},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1999/682},
    editor = {P Flener},
    refereed = {yes},
    volume = {1559},
    booktitle = {Logic Programming, Synthesis and Transformation (Selected Papers)},
    publisher = {Springer-Verlag},
    series = {Lecture Notes in Computer Science},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014