School of Computing

Well-terminating, input-driven logic programs

Jan-Georg Smaus

Technical Report 16-98, University of Kent at Canterbury, November 1998.

Abstract

We identify a class of predicates for which termination does not depend on left-to-right execution. All that is required is that derivations are input-driven that is, in each derivation step, the input arguments of the selected atom do not become instantiated. The method of showing that a predicate is in that class is based on level mappings, closely following the traditional approach for LD derivations. Many predicates terminate under such weak assumptions. Knowing these predicates can be a very useful part of a more comprehensive method of showing termination, which would have to make more specific assumptions about the selection rule.

Download publication 193 kbytes (PostScript)

Bibtex Record

@techreport{645,
author = {Jan-Georg Smaus},
title = {Well-Terminating, Input-Driven Logic Programs},
month = {November},
year = {1998},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1998/645},
    institution = {University of Kent at Canterbury},
    number = {16-98},
}

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

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

Last Updated: 21/03/2014