Automatic Termination Analysis of Logic Programs

13 years 10 months ago
Automatic Termination Analysis of Logic Programs
Abstract This paper describes a general framework for automatic termination analysis of logic programs, where we understand by termination" the niteness of the LD-tree constructed for the program and a given query. A general property of mappings from a certain subset of the branches of an in nite LD-tree into a nite set is proved. From this result several termination theorems are derived, by using di erent nite sets. The rst two are formulated for the predicate dependency and atom dependency graphs. Then a general result for the case of the query-mapping pairs relevant to a program is proved cf. 29,21 . The correctness of the TermiLog system described in 22 follows from it. In this system it is not possible to prove terminationfor programsinvolvingarithmetic predicates, since the usual order for the integers is not well-founded. A new method, which can be easily incorporated in TermiLog or similar systems, is presented, which makes it possible to prove termination for programs i...
Naomi Lindenstrauss, Yehoshua Sagiv
Added 08 Aug 2010
Updated 08 Aug 2010
Type Conference
Year 1997
Where ICLP
Authors Naomi Lindenstrauss, Yehoshua Sagiv
Comments (0)