[Back]

F. Mesnard, E. Payet, U. Neumerkel:
"Non-termination inference for optimal termination conditions of logic programs";
Talk: Onzèmes Journèes Francophones de Programmation Logique, Paris; 2002-05-27 - 2002-05-29; in: " Onzèmes Journèes Francophones de Programmation Logique et Programmation par Constraints (JFPLC`02)", Hermes Science Publications, Paris (2002), ISBN: 2-7462-0477-0; 87 - 104.

in this paper, we present an approach to non-termination inference of logic programs. Our framework relies on an extension of the Lifting Theorem, where some specific argument positions can be instantiated while others are generalized. Atomic left looping queries are generated bottom-up form selected subsets of the binary unfoldings of the program of interest. Then non-termination inference is tailored to attempt proofs of optimality of lieft termination conditions computed by a termination inference tool. For each class of atomic queries not covered by termination condition, the aim is to ensure the existence of one query from this class which leads to an infinite search tree.
When termination and non-termination analysis produce complementary results for a logic procedure with respect ot the left most selection rule and the language used to describe sets of atomic queries.

http://aleph.ub.tuwien.ac.at/F?base=tuw01&func=find-c&ccl_term=AC04404320