Termination analysis of logic programs (Extended abstract)

Termination is well-known to be one of the most intriguing aspects of program verification. Since logic programs are Turing-complete, it follows by the undecidability of the halting problem that there exists no algorithm which, given an arbitrary logic program, decides whether the program terminates. However, one can propose both conditions that are equivalent to termination and their approximations that imply termination and can be verified automatically. This paper briefly discusses these kinds of conditions that were studied in [2]