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. © Springer-Verlag 2004.
CITATION STYLE
Lindenstrauss, N., Sagiv, Y., & Serebrenik, A. (2004). Proving termination for logic programs by the query-mapping pairs approach. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3049, 453–498. https://doi.org/10.1007/978-3-540-25951-0_14
Mendeley helps you to discover research relevant for your work.