School of Computing

Proving Termination of Input-Consuming Logic Programs

Jan-Georg Smaus

Technical Report 10-99, Computing Laboratory, University of Kent at Canterbury, Kent, CT2 7NF, UK, September 1999 Long version of paper with same title at ICLP'99.

Abstract

A class of predicates is identified for which termination does not depend on left-to-right execution. The only assumption about the selection rule is that derivations are input-consuming, that is, in each derivation step, the input arguments of the selected atom do not become instantiated. This assumption is a natural abstraction of previous work on programs with delay declarations. The method for showing that a predicate is in that class is based on level mappings, closely following the traditional approach for LD-derivations. Programs are assumed to be well and nicely moded, which are two widely used concepts for verification. Many predicates terminate under such weak assumptions. Knowing these predicates is useful even for programs where not all predicates have this property.

Download publication 253 kbytes (PostScript)

Bibtex Record

@techreport{873,
author = {Jan-Georg Smaus},
title = {{Proving Termination of Input-Consuming Logic Programs}},
month = {September},
year = {1999},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {Long version of paper with same title at ICLP'99},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1999/873},
    address = {Kent, CT2 7NF, UK},
    institution = {Computing Laboratory, University of Kent at Canterbury},
    number = {10-99},
}

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

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

Last Updated: 21/03/2014