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 .
|Title of host publication||Proceedings of the 19th International Conference on Logic Programming (ICLP'03), 9-13 December 2003, Mumbai, India|
|Place of Publication||Berlin|
|Publication status||Published - 2003|
|Name||Lecture Notes in Computer Science|