Terminyzer: An Automatic Non-termination Analyzer for Large Logic Programs. There have been many studies on termination analysis of logic programs but little has been done to analyze their non-termination, an even more important task, in our opinion. Non-termination analysis examines program execution history when non-termination is suspected and attempts to inform the programmer about possible ways to fix the problem. This paper attempts to fill in the void. We study the problem of non-termination in tabled logic engines with subgoal abstraction, such as XSB, and propose a suite of algorithms, called non-Termination Analyzer, Terminyzer, for automatic detection of non-termination and explaining it to the user. Terminyzer includes several non-termination analysis approaches of different computational complexity. These approaches are all based on analyzing forest logging traces and supply sequences of tabled calls that are likely causes of non-terminating cycles. It also provides the sequences of functors that are applied repeatedly to generate infinitely many answers and thus helps programmers debug large programs by focusing on much smaller subsets of rules. Terminyzer is included in both XSB and F lora -2, and all examples used in this paper are available online.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element