Proving termination with adornments

A. Serebrenik, D. De Schreye

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

    2 Citations (Scopus)

    Abstract

    Termination is well-known to be one of the important aspects of program correctness. Logic programming provides a framework with a strong theoretical basis for tackling this problem. However, due to the declarative formulation of programs, the danger of non-termination may increase. As a result, termination analysis received considerable attention in logic programming. Recently, the study of termination of numerical programs led to the emerging of the adorning technique [7]. This technique implements the well-known divide et impera strategy by distinguishing between different subsets of values for variables, and deriving termination proofs based on these subsets. In this paper we generalise this technique and discuss its applicability to the domain of terms (the Herbrand domain).
    Original languageEnglish
    Title of host publicationProceedings of the 13th International Symposium on Logic Based Program Synthesis and Transformation (LOPSTR 2003), 25-27 August 2003, Uppsala, Sweden
    EditorsM. Bruynooghe
    Place of PublicationBerlin
    PublisherSpringer
    Pages108-109
    ISBN (Print)3-540-22174-3
    DOIs
    Publication statusPublished - 2004

    Publication series

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

    Fingerprint

    Dive into the research topics of 'Proving termination with adornments'. Together they form a unique fingerprint.

    Cite this