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...

• Type: Conference
• Year: 1997
• Where: ICLP
• Authors: Naomi Lindenstrauss, Yehoshua Sagiv
• Keywords: Automated Reasoning, Automatic Termination Analysis, ICLP 1997, Nite Sets, Query-mapping Pairs