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.
|Title of host publication||Program Development in Computational Logic : A Decade of Research Advances in Logic-Based Program Development|
|Editors||M. Bruynooghe, K-K. Lau|
|Place of Publication||Berlin|
|Publication status||Published - 2004|
|Name||Lecture Notes in Computer Science|