Proving termination with adornments

A. Serebrenik, D. De Schreye

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

    2 Citations (Scopus)


    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
    ISBN (Print)3-540-22174-3
    Publication statusPublished - 2004

    Publication series

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


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

    Cite this