A General Framework for Automatic Termination Analysis of Logic Programs

TL;DR

This paper introduces a comprehensive framework for automatically analyzing the termination of logic programs, including new methods for handling arithmetic predicates, enhancing existing tools like TermiLog.

Contribution

It presents a general theoretical framework for termination analysis, extends existing methods to handle arithmetic predicates, and proposes a practical approach for case-based termination proofs.

Findings

Proved a property relating infinite LD-trees to finite mappings.

Derived several termination theorems using dependency graphs.

Developed a new method for proving termination with arithmetic predicates.

Abstract

This paper describes a general framework for automatic termination analysis of logic programs, where we understand by ``termination'' the finitenes s 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 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 result for the case of the query-mapping pairs relevant to a program is proved (cf. \cite{Sagiv,Lindenstrauss:Sagiv}). The correctness of the {\em TermiLog} system described in \cite{Lindenstrauss:Sagiv:Serebrenik} follows from it. In this system it is not possible to prove termination for programs involving arithmetic predicates, since the usual order for the integers is not well-founded. A new method, which can be easily incorporated in {\em TermiLog} or similar systems, is presented, which makes it possible to prove termination for programs involving arithmetic predicates. It is based on combining a finite abstraction of the integers with the technique of the query-mapping pairs, and is essentially capable of dividing a termination proof into several cases, such that a simple termination function suffices for each case. Finally several possible extensions are outlined.