Hostname: page-component-745bb68f8f-mzp66 Total loading time: 0 Render date: 2025-02-11T10:56:51.391Z Has data issue: false hasContentIssue false

On modular termination proofs of general logic programs

Published online by Cambridge University Press:  23 April 2002

ANNALISA BOSSI
Affiliation:
Dipartimento di Informatica, Università Ca’ Foscari di Venezia, via Torino 155, 30172 Venezia, Italy
NICOLETTA COCCO
Affiliation:
Dipartimento di Informatica, Università Ca’ Foscari di Venezia, via Torino 155, 30172 Venezia, Italy
SABINA ROSSI
Affiliation:
Dipartimento di Informatica, Università Ca’ Foscari di Venezia, via Torino 155, 30172 Venezia, Italy
SANDRO ETALLE
Affiliation:
Department of Computer Science, University of Twente, P.O. Box 217, 7500 AE Enschede, The Netherlands and CWI – Center for Mathematics and Computer Science, P.O. Box 94079, 1090 GB Amsterdam, The Netherlands
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

We propose a modular method for proving termination of general logic programs (i.e. logic programs with negation). It is based on the notion of acceptable programs, but it allows us to prove termination in a truly modular way. We consider programs consisting of a hierarchy of modules and supply a general result for proving termination by dealing with each module separately. For programs which are in a certain sense well-behaved, namely well-moded or well-typed programs, we derive both a simple verification technique and an iterative proof method. Some examples show how our system allows for greatly simplified proofs.

Type
Research Article
Copyright
© 2002 Cambridge University Press