Automatic Termination Analysis for Logic Programs

Title: Automatic Termination Analysis for Logic Programs

Abstract: This research focuses on developing a general framework for automatic termination analysis of logic programs. Termination, in this context, refers to the finiteness of the LD-tree constructed for the program and a given query. The study presents a method that abstracts potentially infinite structures to finite ones by mapping partial branches of the LD-tree to elements of a finite set. This approach allows for the derivation of several termination theorems, applicable to predicate dependency, atom dependency graphs, and query-mapping pairs. The research also introduces a new method for showing termination for logic programs involving arithmetic predicates, which is particularly challenging due to the non-well-founded nature of the usual order for integers. This method involves automatic deduction of a finite abstract domain and the application of query-mapping pairs for extending the technique. The study concludes with a discussion of possible extensions and implications of the proposed method.

Main Research Question: How can we develop a general framework for automatic termination analysis of logic programs, particularly for those involving arithmetic predicates?

Methodology: The research employs the technique of abstract interpretation, which involves abstracting potentially infinite structures to finite ones. This is achieved by mapping partial branches of the LD-tree to elements of a finite set. The study presents several termination theorems applicable to predicate dependency, atom dependency graphs, and query-mapping pairs. For logic programs involving arithmetic predicates, the research introduces a new method that involves automatic deduction of a finite abstract domain and the application of query-mapping pairs for extending the technique.

Results: The research presents several termination theorems that can be applied to predicate dependency, atom dependency graphs, and query-mapping pairs. For logic programs involving arithmetic predicates, the study introduces a new method that allows for the automatic deduction of a finite abstract domain and the application of query-mapping pairs for extending the technique.

Implications: The research has significant implications for the field of automatic termination analysis of logic programs. The general framework and the derived termination theorems provide a robust method for checking the termination of logic programs. The new method for showing termination for logic programs involving arithmetic predicates is particularly noteworthy, as it addresses a challenging aspect of this problem. The research also has implications for the development of automated reasoning systems, as it contributes to the understanding of how to effectively handle potentially infinite structures in a finite context.

Link to Article: https://arxiv.org/abs/0012008v1 Authors: arXiv ID: 0012008v1