Proving Termination for Logic Programs by the Query-Mapping Pairs Approach

This paper describes a method for proving termination of to logic programs based on abstract interpretation. The method ry-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.

• Type: Conference
• Year: 2004
• Where: LOPSTR
• Authors: Naomi Lindenstrauss, Yehoshua Sagiv, Alexander Serebrenik
• Keywords: Abstract Interpretation, Logic Programs, LOPSTR 2004, Method Ry-mapping Pairs