Cambridge Journals Online

Cambridge Journals Online
Skip to content
Theory and Practice of Logic Programming (2002), 2: 263-291 Cambridge University Press
Copyright © 2002 Cambridge University Press
doi:10.1017/S1471068402001382
Published online by Cambridge University Press 23Apr2002

On modular termination proofs of general logic programs

ANNALISA BOSSI a1, NICOLETTA COCCO a1, SABINA ROSSI a1 and SANDRO ETALLE a2
a1 Dipartimento di Informatica, Università Ca’ Foscari di Venezia, via Torino 155, 30172 Venezia, Italy
a2 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

Abstract

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.


Key Words: verification; termination; logic programming.

back to top
Cambridge University Press