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 .
|Titel||Proceedings of the 19th International Conference on Logic Programming (ICLP'03), 9-13 December 2003, Mumbai, India|
|Plaats van productie||Berlin|
|ISBN van geprinte versie||3-540-20642-6|
|Status||Gepubliceerd - 2003|
|Naam||Lecture Notes in Computer Science|
|ISSN van geprinte versie||0302-9743|