On termination of binary CLP programs

A. Serebrenik, F. Mesnard

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    2 Citations (Scopus)

    Abstract

    Termination of binary CLP programs has recently become an important question in the termination analysis community. The reason for this is due to the fact that some of the recent approaches to termination of logic programs abstract the input program to a binary CLP program and conclude termination of the input program from termination of the abstracted program. In this paper we introduce a class of binary CLP programs such that their termination can be proved by using linear level mappings. We show that membership to this class is decidable and present a decision procedure. Further, we extend this class to programs such that their termination proofs require a combination of linear functions. In particular we consider as level mappings tuples of linear functions and piecewise linear functions.
    Original languageEnglish
    Title of host publicationLogic based program synthesis and transformation : 14th international symposium, LOPSTR 2004, Verona, Italy, August 26 – 28, 2004 : revised selected papers
    EditorsS. Etalle
    Place of PublicationBerlin
    PublisherSpringer
    Pages231-244
    ISBN (Print)3-540-26655-0
    DOIs
    Publication statusPublished - 2005

    Publication series

    NameLecture Notes in Computer Science
    Volume3573
    ISSN (Print)0302-9743

    Cite this