@inbook{1c51bc3430754720ac6a93058ed18fa2,
title = "Proving termination for logic programs by the query-mapping pairs approach",
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.",
author = "N. Lindenstrauss and Y. Sagiv and A. Serebrenik",
year = "2004",
doi = "10.1007/978-3-540-25951-0\_14",
language = "English",
isbn = "3-540-22152-2",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "453--498",
editor = "M. Bruynooghe and K-K. Lau",
booktitle = "Program Development in Computational Logic : A Decade of Research Advances in Logic-Based Program Development",
address = "Germany",
}