Unfolding the mystery of Mergesort

N. Lindenstrauss, Y. Sagiv, A. Serebrenik

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

    7 Citations (Scopus)


    This paper outlines a fully automatic transformation for proving termination of queries to a class of logic programs, for which existing methods do not work directly. The transformation consists of creating adorned clauses and unfolding. In general, the transformation may improve termination behavior by pruning infinite branches from the LD-tree. Conditions are given under which the transformation preserves termination behavior. The work presented here has been done in the framework of the TermiLog system, and it complements the algorithms described in [12].
    Original languageEnglish
    Title of host publicationProceedings of the 7th International Workshop on Logic Programming Synthesis and Transformation (LOPSTR'97), 10-12 July 1997, Leuven, Belgium
    EditorsN.E. Fuchs
    Place of PublicationBerlin
    ISBN (Print)3-540-65074-1
    Publication statusPublished - 1997

    Publication series

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


    Dive into the research topics of 'Unfolding the mystery of Mergesort'. Together they form a unique fingerprint.

    Cite this