Unfolding the mystery of Mergesort

N. Lindenstrauss, Y. Sagiv, A. Serebrenik

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

    7 Citations (Scopus)

    Abstract

    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
    PublisherSpringer
    Pages206-225
    ISBN (Print)3-540-65074-1
    DOIs
    Publication statusPublished - 1997

    Publication series

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

    Cite this