CW 537

Dean Voets and Danny De Schreye
A new approach to non-termination analysis of Logic Programs

Abstract

In this paper, we present a new approach to non-termination analysis of logic programs based on moded SLDNF-resolution. Moded SLDNF-resolution is a symbolic execution for moded goals developed for termination prediction. To prove non-termination, we use a complete loop checker to create a finite symbolic derivation tree of a logic program and moded query. Then, we check if this derivation tree contains an infinite loop, using a new non-termination condition. We implemented this approach and tested it on the benchmark from the Termination Competition of 2007. The results are very satisfactory: our tool is able to prove non-termination and construct non-terminating queries for all non-terminating benchmark programs, and thus, significantly improves on the results of the only other non-termination analyzer, NTI.

report.pdf (324K) / mailto: D. Voets