Inference of termination conditions for numerical loops in prolog

A. Serebrenik, D. De Schreye

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

    7 Citations (Scopus)

    Abstract

    Numerical computations form an essential part of almost any real-world program. Clearly, in order for a termination analyser to be of practical use it should contain a mechanism for inferring termination of such computations. However, this topic attracted less attention of the research community. In this work we concentrate on automatic termination inference for logic programs depending on numerical computations. Dershowitz et al. [8] showed that termination of general numerical computations, for instance on floating point numbers, may be counter-intuitive, i.e., the observed behaviour does not necessarily coincide with the theoretically expected one. Thus, we restrict ourselves to integer computations only.
    Original languageEnglish
    Title of host publicationProceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR2001), 3-7 December 2001, Havana, Cuba
    EditorsR. Nieuwenhuis, A. Voronkov
    Place of PublicationBerlin
    PublisherSpringer
    Pages654-669
    ISBN (Print)3-540-42957-3
    DOIs
    Publication statusPublished - 2001

    Publication series

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

    Cite this