Proving termination for logic programs by the query-mapping pairs approach

N. Lindenstrauss, Y. Sagiv, A. Serebrenik

    Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

    10 Citations (Scopus)

    Abstract

    This paper describes a method for proving termination of queries to logic programs based on abstract interpretation. The method uses query-mapping pairs to abstract the relation between calls in the LD-tree associated with the program and query. Any well founded partial order for terms can be used to prove the termination. The ideas of the query-mapping pairs approach have been implemented in SICStus Prolog in a system called TermiLog, which is available on the web. Given a program and query pattern the system either answers that the query terminates or that there may be non-termination. The advantages of the method are its conceptual simplicity and the fact that it does not impose any restrictions on the programs.
    Original languageEnglish
    Title of host publicationProgram Development in Computational Logic : A Decade of Research Advances in Logic-Based Program Development
    EditorsM. Bruynooghe, K-K. Lau
    Place of PublicationBerlin
    PublisherSpringer
    Pages453-498
    ISBN (Print)3-540-22152-2
    DOIs
    Publication statusPublished - 2004

    Publication series

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

    Cite this