On modular termination proofs of general logic programs

A. Bossi, N. Cocco, S. Rossi, S. Etalle

    Research output: Contribution to journalArticleAcademicpeer-review

    11 Citations (Scopus)
    1 Downloads (Pure)

    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.
    Original languageEnglish
    Pages (from-to)263-291
    JournalTheory and Practice of Logic Programming
    Volume2
    Issue number3
    DOIs
    Publication statusPublished - 2002

    Fingerprint Dive into the research topics of 'On modular termination proofs of general logic programs'. Together they form a unique fingerprint.

    Cite this