A general framework for automatic termination analysis of logic programs

This paper describes a general framework for automatic termination analysis of logic programs, where we understand by "termination" the finiteness of the LD-tree constructed for the program and a given query. A general proper ty of mappings from a certain subset of the branches of an infinite LD-tree into a finite set is proved. From this result several termination theorems are derived, by using different finite sets. The first two are formulated for the predicate dependency and atom dependency graphs. Then a general res ult for the case of the query-mapping pairs relevant to a program is proved (cf. C29, 21]). The correctness of the Termilog system described in [22] f ollows from it. In this system it is not possible to prove termination for programs involving arithmetic predicates, since the usual order for the int egers is not well-founded. A new method, which can be easily incorporated i n Termilog or similar systems, is presented, which makes it possible to pro ve termination for programs involving arithmetic predicates. It is based on combining a finite abstraction of the integers with the technique of the q uery-mapping pairs, and is essentially capable of dividing. a termination p roof into several cases, such that a simple termination function suffices f or each case. Finally several possible extensions are outlined. This resear ch has been partially supported by grants from the Israel Science Foundatio n.