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.  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.
|Title of host publication||Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR2001), 3-7 December 2001, Havana, Cuba|
|Editors||R. Nieuwenhuis, A. Voronkov|
|Place of Publication||Berlin|
|Publication status||Published - 2001|
|Name||Lecture Notes in Computer Science|